References

  1. Andreas Abel (2006): Implementing a normalizer using sized heterogeneous types. In: In Workshop on Mathematically Structured Functional Programming, MSFP, doi:10.1017/S0956796809007266.
  2. 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.
  3. Robin Adams (2004): A Modular Hierarchy of Logical Frameworks.
  4. R.M. Amadio & P.L. Curien (1998): Domains and lambda-calculi. Cambridge tracts in theoretical computer science. Cambridge University Press, doi:10.1017/CBO9780511983504.
  5. 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.
  6. 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.
  7. Rene David & Karim Nour (2003): A short proof of the strong normalization of the simply typed lambdamu-calculus. SCHEDAE INFORMATICAE 12, pp. 27–33.
  8. Harley Eades & Aaron Stump (2010): Hereditary Substitution for Stratified System F. In: Proof-Search in Type Theories (PSTT).
  9. Jean-Yves Girard, Yves Lafont & Paul Taylor (1989): Proofs and Types (Cambridge Tracts in Theoretical Computer Science). Cambridge University Press.
  10. Harley Eades II & Aaron Stump (2011): Using the Hereditary Substitution Function in Normalization Proofs. Available at http://metatheorem.org/wp-content/papers/qual_companion_report.pdf.
  11. Felix Joachimski & Ralph Matthes (1999): Short Proofs of Normalization for the simply-typed lambda-calculus, permutative conversions and Gödel's T.
  12. 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.
  13. D. Leivant (1991): Finitely stratified polymorphism. Inf. Comput. 93(1), pp. 93–113, doi:10.1016/0890-5401(91)90053-5.
  14. 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.
  15. 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.
  16. 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.
  17. 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.
  18. 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.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org