Categorical reconstruction of a reduction free normalization proof
T Altenkirch, M Hofmann, T Streicher - … , August 7–11, 1995 Proceedings 6, 1995 - Springer
T Altenkirch, M Hofmann, T Streicher
Category Theory and Computer Science: 6th International Conference, CTCS'95 …, 1995•SpringerCategorical reconstruction of a reduction free normalization proof Page 1 Categorical
reconstruction of a reduction free normalization proof *. Thorsten Altenkirch 1, Martin Hofmann
2 ** and Thomas Streicher 3 1 Chalmers University of Technology, G6teborg, Sweden email :
alt i9 chalmers, se 2 University of Edinburgh, Scotland email : mxh~dcs, ed. ac .Ilk 3
Technische Hochschule Darmstadt, Germany email : streicher@mathematik.th-darmstadt.de 1
Introduction We present a categorical proof of the normalization theorem for simply typed A-calculus …
reconstruction of a reduction free normalization proof *. Thorsten Altenkirch 1, Martin Hofmann
2 ** and Thomas Streicher 3 1 Chalmers University of Technology, G6teborg, Sweden email :
alt i9 chalmers, se 2 University of Edinburgh, Scotland email : mxh~dcs, ed. ac .Ilk 3
Technische Hochschule Darmstadt, Germany email : streicher@mathematik.th-darmstadt.de 1
Introduction We present a categorical proof of the normalization theorem for simply typed A-calculus …
We present a categorical proof of the normalization theorem for simply typed A-calculus, ie we derive a computable function nf which assigns to every typed A-term a normal form, st
Springer