|
| << vorige |
Tijdschrift beschrijving
Alle jaargangen van het bijbehorende tijdschrift
Alle afleveringen van het bijbehorende jaargang
Alle artikelen van de bijbehorende aflevering
Details van artikel 9 van 9 gevonden artikelen
| Titel: |
Untyped Algorithmic Equality for Martin-Löf's Logical Framework with Surjective Pairs |
| Auteur: |
Abel, Andreas Coquand, Thierry |
| Verschenen in: |
Fundamenta informaticae |
| Paginering: | Jaargang 77 (2007) nr. 4 pagina's 345-395 |
| Jaar: |
2007-06-06 |
| Inhoud: |
Martin-Löf's Logical Framework is extended by strong Σ-types and presented via judgmental equality with rules for extensionality and surjective pairing. Soundness of the framework rules is proven via a generic PER model on untyped terms. An algorithmic version of the framework is given through an untyped βη-equality test and a bidirectional type checking algorithm. Completeness is proven by instantiating the PER model with η-equality on β-normal forms, which is shown equivalent to the algorithmic equality. |
| Uitgever: |
IOS Press |
| Bronbestand: |
Elektronische Wetenschappelijke Tijdschriften |
Details van artikel 9 van 9 gevonden artikelen
| << vorige |