package coq-tait
A normalization proof a la Tait for simply-typed lambda-calculus
Install
Dune Dependency
Authors
Maintainers
Sources
v8.10.0.tar.gz
md5=7620616203526e7d85b6e100d8bfa32b
Description
This is a formalization of Berger's TLCA'93 paper, with complete proofs of the axioms and an extraction of a normalization program close to N.B.E.
Tags
keyword: normalization keyword: lambda calculus keyword: extraction keyword: Tait proof keyword: normalization by evalution keyword: type theory category: Mathematics/Logic/Type theory category: Computer Science/Lambda Calculi category: Miscellaneous/Extracted Programs/Type checking unification and normalization date: 2004Published: 07 Dec 2019
On This Page