Tyck till om SwePub Sök
här!
Sökning: id:"swepub:oai:gup.ub.gu.se/175708" >
Untyped algorithmic...
Untyped algorithmic equality for Martin-Löf's logical framework with surjective pairs
-
Abel, Andreas, 1974 (författare)
-
- Coquand, Thierry, 1961 (författare)
- Gothenburg University,Göteborgs universitet,Institutionen för data- och informationsteknik, datavetenskap, programmeringslogik (GU),Department of Computer Science and Engineering, Computing Science, Programming Logic,University of Gothenburg
-
(creator_code:org_t)
- 2007
- 2007
- Engelska.
-
Ingår i: Fundamenta Informaticae. - 0169-2968. ; 77:4, s. 345-395
- Relaterad länk:
-
https://gup.ub.gu.se...
-
visa fler...
-
https://research.cha...
-
visa färre...
Abstract
Ämnesord
Stäng
- Martin-Löf's Logical Framework is extended by strong Sigma-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 beta eta-equality test and a bidirectional type checking algorithm. Completeness is proven by instantiating the PER model with eta-equality on beta-normal forms, which is shown equivalent to the algorithmic equality.
Ämnesord
- NATURVETENSKAP -- Data- och informationsvetenskap (hsv//swe)
- NATURAL SCIENCES -- Computer and Information Sciences (hsv//eng)
Nyckelord
- lambda-calculus
- lambda-calculus
Publikations- och innehållstyp
- ref (ämneskategori)
- art (ämneskategori)
Hitta via bibliotek
Till lärosätets databas