Weak βη-Normalization and Normalization by Evaluation for System F
A Abel - International Conference on Logic for Programming …, 2008 - Springer
International Conference on Logic for Programming Artificial Intelligence and …, 2008•Springer
Weak βη-Normalization and Normalization by Evaluation for System F Page 1 Weak βη-Normalization
and Normalization by Evaluation for System F Andreas Abel Department of Computer Science
Ludwig-Maximilians-University Munich Abstract. A general version of the fundamental theorem
for System F is presented which can be instantiated to obtain proofs of weak β- and
βη-normalization and normalization by evaluation. 1 Introduction and Related Work
Dependently typed lambda-calculi have been successfully used as proof languages in proof …
and Normalization by Evaluation for System F Andreas Abel Department of Computer Science
Ludwig-Maximilians-University Munich Abstract. A general version of the fundamental theorem
for System F is presented which can be instantiated to obtain proofs of weak β- and
βη-normalization and normalization by evaluation. 1 Introduction and Related Work
Dependently typed lambda-calculi have been successfully used as proof languages in proof …
Abstract
A general version of the fundamental theorem for System F is presented which can be instantiated to obtain proofs of weak β- and βη-normalization and normalization by evaluation.
Springer