A Logical Framework with Explicit Conversions

DOI10.1016/j.entcs.2007.11.011zbMath1278.03058OpenAlexW2163562725MaRDI QIDQ2871837

Herman Geuvers, Freek Wiedijk

Publication date: 10 January 2014

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

Full work available at URL: https://doi.org/10.1016/j.entcs.2007.11.011

zbMATH Keywords

type theorylogical frameworkconvertibility\(\lambda H\)\(\lambda P\)explicit type conversion

Mathematics Subject Classification ID

Logic in computer science (03B70) Combinatory logic and lambda calculus (03B40)

Uses Software

• Coq
• Twelf
• Automath

Cites Work

• The typed lambda-calculus is not elementary recursive
• Selected papers on AUTOMATH, dedicated to N. G. de Bruijn
• Pure type systems with judgemental equality
• Proof by computation in the Coq system
• Unnamed Item
• Unnamed Item
• Unnamed Item

This page was built for publication: A Logical Framework with Explicit Conversions