Paper Info
Title
Parigot's Second Order lambda-mu-Calculus and Inductive Types
Abstract
. A new proof of strong normalization of Parigot's (secondorder) -calculus is given by a reduction-preserving embedding intosystem F (second order polymorphic -calculus). The main idea is touse the least stable supertype for any type. These non-strictly positiveinductive types and their associated iteration principle are available insystem F, and allow to give a translation vaguely related to CPS translations(corresponding to the Kolmogorov embedding of classical logicinto...
Year
Venue
Keywords
2001
TLCA
second order,polymorphism
Field
DocType
Citations 
Discrete mathematics,Computer science,Calculus,Lambda-mu calculus
Conference
0
PageRank 
References 
Authors
0.34
6
1
Name
Order
Citations
PageRank
Ralph Matthes120121.67