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
Sitemap
To content Read more about how we use cookies on gu.se

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

Abstract

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
Share:

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?