References

  1. Jean-Philippe Bernardy & Marc Lasson (2011): Realizability and Parametricity in Pure Type Systems. In: Martin Hofmann: Foundations of Software Science and Computational Structures - 14th International Conference, FOSSACS 2011, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2011, Saarbrücken, Germany, March 26-April 3, 2011. Proceedings, Lecture Notes in Computer Science 6604. Springer, pp. 108–122, doi:10.1007/978-3-642-19805-2_8.
  2. Richard S. Bird & Oege de Moor (1997): Algebra of programming. Prentice Hall International series in computer science. Prentice Hall, doi:10.1017/S095679689922326X.
  3. N.G. de Bruijn (1994): A Survey of the Project Automath**Reprinted from: Seldin, J. P. and Hindley, J. R., eds., To H. B. Curry: Essays on Combinatory Logic, Lambda Calculus and Formalism, p. 579-606, by courtesy of Academic Press Inc., Orlando.. In: R.P. Nederpelt, J.H. Geuvers & R.C. de Vrijer: Selected Papers on Automath, Studies in Logic and the Foundations of Mathematics 133. Elsevier, pp. 141 – 161, doi:10.1016/S0049-237X(08)70203-9.
  4. Robert L. Constable, Stuart F. Allen, Mark Bromley, Rance Cleaveland, J. F. Cremer, R. W. Harper, Douglas J. Howe, Todd B. Knoblock, N. P. Mendler, Prakash Panangaden, James T. Sasaki & Scott F. Smith (1986): Implementing mathematics with the Nuprl proof development system. Prentice Hall.
  5. Larry Diehl, Denis Firsov & Aaron Stump (2018): Generic Zero-cost Reuse for Dependent Types. Proc. ACM Program. Lang. 2(ICFP), pp. 104:1–104:30, doi:10.1145/3236799.
  6. Denis Firsov, Richard Blair & Aaron Stump (2018): Efficient Mendler-Style Lambda-Encodings in Cedille. In: Jeremy Avigad & Assia Mahboubi: Interactive Theorem Proving - 9th International Conference, ITP 2018, Held as Part of the Federated Logic Conference, FloC 2018, Oxford, UK, July 9-12, 2018, Proceedings, Lecture Notes in Computer Science 10895. Springer, pp. 235–252, doi:10.1007/978-3-319-94821-8_14.
  7. Denis Firsov & Aaron Stump (2018): Generic Derivation of Induction for Impredicative Encodings in Cedille. In: Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, CPP 2018. ACM, New York, NY, USA, pp. 215–227, doi:10.1145/3167087.
  8. Herman Geuvers (2001): Induction Is Not Derivable in Second Order Dependent Type Theory. In: Typed Lambda Calculi and Applications (TLCA), pp. 166–181, doi:10.1007/3-540-45413-6_16.
  9. Jean-Yves Girard (1972): Interprétation functionelle et élimination des coupures dans larithmétique dordre supérieure. Université Paris VII.
  10. J. Roger Hindley & Jonathan P. Seldin (2008): Lambda-Calculus and Combinators: An Introduction, 2 edition. Cambridge University Press, New York, NY, USA, doi:10.1017/CBO9780511809835.
  11. A. Kopylov (2003): Dependent intersection: a new way of defining records in type theory. In: 18th Annual IEEE Symposium of Logic in Computer Science, 2003. Proceedings., pp. 86–95, doi:10.1109/LICS.2003.1210048.
  12. Zhaohui Luo (1990): An extended calculus of constructions. University of Edinburgh, UK. Available at http://hdl.handle.net/1842/12487.
  13. P. Martin-Löf (1975): An intuitionisitc theory of types, Predicative part. In: Logic Colloquium 1973, pp. 73–118.
  14. N. P. Mendler (1991): Inductive Types and Type Constraints in the Second-Order lambda Calculus. Ann. Pure Appl. Logic 51(1-2), pp. 159–172, doi:10.1016/0168-0072(91)90069-X.
  15. Dale Miller & Alwen Tiu (2005): A proof theory for generic judgments. ACM Trans. Comput. Log. 6(4), pp. 749–783, doi:10.1145/1094622.1094628.
  16. Alexandre Miquel (2001): The Implicit Calculus of Constructions Extending Pure Type Systems with an Intersection Type Binder and Subtyping. In: Samson Abramsky: Typed Lambda Calculi and Applications. Springer Berlin Heidelberg, Berlin, Heidelberg, pp. 344–359, doi:10.1007/3-540-45413-6_27.
  17. John C. Mitchell & Eugenio Moggi (1991): Kripke-Style Models for Typed lambda Calculus. Ann. Pure Appl. Logic 51(1-2), pp. 99–124, doi:10.1016/0168-0072(91)90067-V.
  18. Christine Paulin-Mohring (1993): Inductive Definitions in the System Coq - Rules and Properties. In: Proceedings of the International Conference on Typed Lambda Calculi and Applications, TLCA '93. Springer-Verlag, London, UK, UK, pp. 328–345, doi:10.1007/BFb0037116.
  19. Frank Pfenning & Conal Elliott (1988): Higher-Order Abstract Syntax. In: Richard L. Wexelblat: Proceedings of the ACM SIGPLAN'88 Conference on Programming Language Design and Implementation (PLDI), Atlanta, Georgia, USA, June 22-24, 1988. ACM, pp. 199–208, doi:10.1145/53990.54010.
  20. Frank Pfenning & Christine Paulin-Mohring (1989): Inductively Defined Types in the Calculus of Constructions. In: M. Main, A. Melton, M. Mislove & D. Schmidt: Proceedings of the Fifth Conference on the Mathematical Foundations of Programming Semantics, Tulane University, New Orleans, Louisiana. Springer-Verlag LNCS 442, pp. 209–228, doi:10.1007/BFb0040259.
  21. Benjamin C. Pierce & David N. Turner (2000): Local type inference. ACM Trans. Program. Lang. Syst. 22(1), pp. 1–44, doi:10.1145/345099.345100.
  22. John C. Reynolds (1974): Towards a theory of type structure. In: Bernard Robinet: Programming Symposium, Proceedings Colloque sur la Programmation, Paris, France, April 9-11, 1974, Lecture Notes in Computer Science 19. Springer, pp. 408–423, doi:10.1007/3-540-06859-7_148.
  23. John C. Reynolds (1983): Types, Abstraction and Parametric Polymorphism. In: IFIP Congress, pp. 513–523.
  24. Carsten Schürmann, Joëlle Despeyroux & Frank Pfenning (2001): Primitive recursion for higher-order abstract syntax. Theor. Comput. Sci. 266(1-2), pp. 1–57, doi:10.1016/S0304-3975(00)00418-7.
  25. Peter Selinger (2002): The lambda calculus is algebraic. J. Funct. Program. 12(6), pp. 549–566, doi:10.1017/S0956796801004294.
  26. Aaron Stump (2017): The calculus of dependent lambda eliminations. Journal of Functional Programming 27, pp. e14, doi:10.1017/S0956796817000053.
  27. Aaron Stump (2018): From realizability to induction via dependent intersection. Ann. Pure Appl. Logic 169(7), pp. 637–655, doi:10.1016/j.apal.2018.03.002.
  28. Aaron Stump (2018): Syntax and Semantics of Cedille. CoRR abs/1806.04709. Available at http://arxiv.org/abs/1806.04709.
  29. Aaron Stump (2018): Syntax and Typing for Cedille Core. CoRR abs/1811.01318. Available at http://arxiv.org/abs/1811.01318.
  30. Aaron Stump & Peng Fu (2016): Efficiency of lambda-encodings in total type theory. Journal of Functional Programming 26, doi:10.1017/S0956796816000034.
  31. The Agda development team (2016): Agda. Available at http://wiki.portal.chalmers.se/agda/pmwiki.php. Version 2.5.1.
  32. The Coq development team (2016): The Coq proof assistant reference manual. LogiCal Project. Available at http://coq.inria.fr. Version 8.5.
  33. Philip Wadler (1990): Recursive types for free!. Available at http://homepages.inf.ed.ac.uk/wadler/papers/free-rectypes/free-rectypes.txt.
  34. Geoffrey Washburn & Stephanie Weirich (2008): Boxes go bananas: Encoding higher-order abstract syntax with parametric polymorphism. J. Funct. Program. 18(1), pp. 87–140, doi:10.1017/S0956796807006557.
  35. J. B. Wells (1999): Typability and Type Checking in System F are Equivalent and Undecidable. Ann. Pure Appl. Logic 98(1-3), pp. 111–156, doi:10.1016/S0168-0072(98)00047-5.
  36. Benjamin Werner (1994): Une Théorie des Constructions Inductives. Université Paris-Diderot - Paris VII. Available at https://tel.archives-ouvertes.fr/tel-00196524.
  37. Freek Wiedijk (2012): Pollack-inconsistency. Electr. Notes Theor. Comput. Sci. 285, pp. 85–100, doi:10.1016/j.entcs.2012.06.008.

Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org