CPL - Chalmers Publication Library
| Utbildning | Forskning | Styrkeområden | Om Chalmers | In English In English Ej inloggad.

Normalization by Evaluation for Martin-Löf Type Theory with Equality Judgements

Andreas Abel ; Thierry Coquand ; Peter Dybjer (Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers))
Proceedings of 22nd IEEE Annual Symposium on Logic in ComputerScience, Wroclaw, Poland, July 2007. p. 3-12. (2007)
[Artikel, refereegranskad vetenskaplig]

The decidability of equality is proved for Martin-Löf type theory with a universe a la Russell and typed beta-eta-equality judgements. A corollary of this result is that the constructor for dependent function types is injective, a property which is crucial for establishing the correctness of the type-checking algorithm. The decision procedure uses normalization by evaluation, an algorithm which first interprets terms in a domain with untyped semantic elements and then extracts normal forms. The correctness of this algorithm is established using a PER-model and a logical relation between syntax and semantics.



Denna post skapades 2007-05-07. Senast ändrad 2016-10-18.
CPL Pubid: 41354

 

Läs direkt!


Länk till annan sajt (kan kräva inloggning)


Institutioner (Chalmers)

Institutionen för data- och informationsteknik, datavetenskap, programmeringslogik (GU) (GU)
Institutionen för data- och informationsteknik, Datavetenskap, Programmeringslogik (Chalmers)

Ämnesområden

Datalogi

Chalmers infrastruktur