Andreas Abel (2006):
Implementing a normalizer using sized heterogeneous types.
In: In Workshop on Mathematically Structured Functional Programming, MSFP,
doi:10.1017/S0956796809007266.
Andreas Abel & Dulma Rodriguez (2008):
Syntactic Metatheory of Higher-Order Subtyping.
In: Proceedings of the 22nd international workshop on Computer Science Logic,
CSL '08.
Springer-Verlag,
Berlin, Heidelberg,
pp. 446–460,
doi:10.1007/978-3-540-87531-4_32.
Robin Adams (2004):
A Modular Hierarchy of Logical Frameworks.
R.M. Amadio & P.L. Curien (1998):
Domains and lambda-calculi.
Cambridge tracts in theoretical computer science.
Cambridge University Press,
doi:10.1017/CBO9780511983504.
G. Barthe, J. Hatcliff & M. Heine Sørensen (1997):
A notion of classical pure type system (preliminary version).
Electronic Notes in Theoretical Computer Science 6,
pp. 4–59,
doi:10.1016/S1571-0661(05)80170-7.
Gilles Barthe, John Hatcliff & Morten Heine Sørensen (2001):
Weak normalization implies strong normalization in a class of non-dependent pure type systems.
Theoretical Computer Science 269(1-2),
pp. 317 – 361,
doi:10.1016/S0304-3975(01)00012-3.
Rene David & Karim Nour (2003):
A short proof of the strong normalization of the simply typed lambdamu-calculus.
SCHEDAE INFORMATICAE 12,
pp. 27–33.
Harley Eades & Aaron Stump (2010):
Hereditary Substitution for Stratified System F.
In: Proof-Search in Type Theories (PSTT).
Jean-Yves Girard, Yves Lafont & Paul Taylor (1989):
Proofs and Types (Cambridge Tracts in Theoretical Computer Science).
Cambridge University Press.
Felix Joachimski & Ralph Matthes (1999):
Short Proofs of Normalization for the simply-typed lambda-calculus, permutative conversions and Gödel's T.
Chantal Keller & Thorsten Altenkirch (2010):
Hereditary substitutions for simple types, formalized.
In: Proceedings of the third ACM SIGPLAN workshop on Mathematically structured functional programming,
MSFP '10.
ACM,
New York, NY, USA,
pp. 3–10,
doi:10.1145/1863597.1863601.
D. Leivant (1991):
Finitely stratified polymorphism.
Inf. Comput. 93(1),
pp. 93–113,
doi:10.1016/0890-5401(91)90053-5.
Jean-Jacques Lévy (1976):
An algebraic interpretation of the λβK-calculus; and an application of a labelled λ-calculus.
Theoretical Computer Science 2(1),
pp. 97 – 114,
doi:10.1016/0304-3975(76)90009-8.
Michel Parigot (1992):
Lambda-Mu-Calculus: An algorithmic interpretation of classical natural deduction.
In: Andrei Voronkov: Logic Programming and Automated Reasoning,
Lecture Notes in Computer Science 624.
Springer Berlin / Heidelberg,
pp. 190–201,
doi:10.1007/BFb0013061.
Michel Parigot (1997):
Proofs of Strong Normalization for Second Order Classical Natural Deduction.
Journal of Symbolic Logic 62(4),
pp. 1461–1479,
doi:10.2307/2275652.
Jakob Rehof & Morten Heine Sørensen (1994):
The LambdaDelta-calculus.
In: Proceedings of the International Conference on Theoretical Aspects of Computer Software,
TACS '94.
Springer-Verlag,
London, UK,
pp. 516–542,
doi:10.1007/3-540-57887-0_113.
Kevin Watkins, Iliano Cervesato, Frank Pfenning & David Walker (2004):
A Concurrent Logical Framework: The Propositional Fragment.
In: Stefano Berardi, Mario Coppo & Ferruccio Damiani: Types for Proofs and Programs,
Lecture Notes in Computer Science 3085.
Springer Berlin / Heidelberg,
pp. 355–377,
doi:10.1007/978-3-540-24849-1_23.