To the top

Page Manager: Webmaster
Last update: 9/11/2012 3:13 PM

Tell a friend about this page
Print version

Untyped algorithmic equal… - University of Gothenburg, Sweden Till startsida
To content Read more about how we use cookies on

Untyped algorithmic equality for Martin-Löf's logical framework with surjective pairs

Journal article
Authors Andreas Abel
Thierry Coquand
Published in Fundamenta Informaticae
Volume 77
Issue 4
Pages 345-395
ISSN 0169-2968
Publication year 2007
Published at Department of Computer Science and Engineering, Computing Science, Programming Logic
Pages 345-395
Language en
Keywords lambda-calculus
Subject categories Computer and Information Science


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.

Page Manager: Webmaster|Last update: 9/11/2012

The University of Gothenburg uses cookies to provide you with the best possible user experience. By continuing on this website, you approve of our use of cookies.  What are cookies?