package coq-tait

  1. Overview
  2. No Docs
A normalization proof a la Tait for simply-typed lambda-calculus

Install

Dune Dependency

github.com Edit opam file Versions (6)

Authors

  1. P
    Pierre Letouzey
  2. H
    Helmut Schwichtenberg

Maintainers

  1. H
    Hugo.Herbelin@inria.fr

Sources

v8.7.0.tar.gz
md5=df90e5a8502acbb2f488408ed30528df

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

Published: 11 Jan 2019

Dependencies (2)

  1. coq >= "8.7" & < "8.8~"
  2. ocaml

Dev Dependencies

None

Used by

None

Conflicts

None