A formalization of the strong normalization proof for System F in LEGO

Publisher Website

25 January 2006

book chapter
Published by Springer Nature

p. 13-28
https://doi.org/10.1007/bfb0037095

Abstract

No abstract available

This publication has 3 references indexed in Scilit:

Inductively defined types
Lecture Notes in Computer Science, 1990
Confluent Reductions: Abstract Properties and Applications to Term Rewriting Systems
Journal of the ACM, 1980
Lambda calculus notation with nameless dummies, a tool for automatic formula manipulation, with application to the Church-Rosser theorem
Indagationes Mathematicae, 1972