Categorical reconstruction of a reduction free normalization proof

Authors:

Publisher website

1 January 1995

book chapter
Published by Springer Nature

p. 182-199
DOI:10.1007/3-540-60164-3_27

Abstract

No abstract available

Keywords

This publication has 5 references indexed in Scilit:

βη-Equality for coproducts
1995
An algorithm for testing conversion in type theory
1991
Kripke-style models for typed lambda calculus
Annals of Pure and Applied Logic, 1991
An inverse of the evaluation functional for typed lambda -calculus
1991
Semantical Analysis of Intuitionistic Logic I
1965