### Skapa referens, olika format (klipp och klistra)

**Harvard**

Abel, A., Vezzosi, A. och Winterhalter, T. (2017) *Normalization by evaluation for sized dependent types*.

** BibTeX **

@conference{

Abel2017,

author={Abel, Andreas and Vezzosi, Andrea and Winterhalter, Theo},

title={Normalization by evaluation for sized dependent types},

booktitle={Proceedings of the ACM on Programming Languages},

pages={33:1--33:3},

abstract={Sized types have been developed to make termination checking more perspicuous, more powerful, and more modular by integrating termination into type checking. In dependently-typed proof assistants where proofs by induction are just recursive functional programs, the termination checker is an integral component of the trusted core, as validity of proofs depend on termination. However, a rigorous integration of full-fledged sized types into dependent type theory is lacking so far. Such an integration is non-trivial, as explicit sizes in proof terms might get in the way of equality checking, making terms appear distinct that should have the same semantics.
In this article, we integrate dependent types and sized types with higher-rank size polymorphism, which is essential for generic programming and abstraction. We introduce a size quantifier (\forall) which lets us ignore sizes in terms for equality checking, alongside with a second quantifier Î for abstracting over sizes that do affect the semantics of types and terms. Judgmental equality is decided by an adaptation of normalization-by-evaluation for our new type theory, which features type shape-directed reflection and reification. It follows that subtyping and type checking of normal forms are decidable as well, the latter by a bidirectional algorithm.},

year={2017},

keywords={dependent types, eta-equality, normalization-by-evaluation, proof irrelevance, sized types, subtyping, universes},

}

** RefWorks **

RT Conference Proceedings

SR Electronic

ID 252072

A1 Abel, Andreas

A1 Vezzosi, Andrea

A1 Winterhalter, Theo

T1 Normalization by evaluation for sized dependent types

YR 2017

T2 Proceedings of the ACM on Programming Languages

SP 331

AB Sized types have been developed to make termination checking more perspicuous, more powerful, and more modular by integrating termination into type checking. In dependently-typed proof assistants where proofs by induction are just recursive functional programs, the termination checker is an integral component of the trusted core, as validity of proofs depend on termination. However, a rigorous integration of full-fledged sized types into dependent type theory is lacking so far. Such an integration is non-trivial, as explicit sizes in proof terms might get in the way of equality checking, making terms appear distinct that should have the same semantics.
In this article, we integrate dependent types and sized types with higher-rank size polymorphism, which is essential for generic programming and abstraction. We introduce a size quantifier (\forall) which lets us ignore sizes in terms for equality checking, alongside with a second quantifier Î for abstracting over sizes that do affect the semantics of types and terms. Judgmental equality is decided by an adaptation of normalization-by-evaluation for our new type theory, which features type shape-directed reflection and reification. It follows that subtyping and type checking of normal forms are decidable as well, the latter by a bidirectional algorithm.

LA eng

DO 10.1145/3110277

LK http://doi.acm.org/10.1145/3110277

LK http://publications.lib.chalmers.se/records/fulltext/252072/local_252072.pdf

OL 30