Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory

DOI10.1007/978-3-540-70594-9_4zbMath1157.68025OpenAlexW18232636MaRDI QIDQ3521979

Thierry Coquand, Peter Dybjer, Andreas Abel

Publication date: 28 August 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-70594-9_4

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (8)

Pure type systems with explicit substitutions ⋮ A Partial Type Checking Algorithm for Type:Type ⋮ Dependent Types at Work ⋮ Unnamed Item ⋮ Type Theory Should Eat Itself ⋮ A Modular Type-Checking Algorithm for Type Theory with Singleton Types and Proof Irrelevance ⋮ Typed Applicative Structures and Normalization by Evaluation for System F ω ⋮ The Confluent Terminating Context-Free Substitutive Rewriting System for the lambda-Calculus with Surjective Pairing and Terminal Type

Uses Software

• Coq
• Twelf
• Epigram
• Agda

This page was built for publication: Verifying a Semantic βη-Conversion Test for Martin-Löf Type Theory