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.
Richard S. Bird & Oege de Moor (1997):
Algebra of programming.
Prentice Hall International series in computer science.
Prentice Hall,
doi:10.1017/S095679689922326X.
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.
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.
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.
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.
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.
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.
Jean-Yves Girard (1972):
Interprétation functionelle et élimination des coupures dans larithmétique dordre supérieure.
Université Paris VII.
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.
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.
Zhaohui Luo (1990):
An extended calculus of constructions.
University of Edinburgh, UK.
Available at http://hdl.handle.net/1842/12487.
P. Martin-Löf (1975):
An intuitionisitc theory of types, Predicative part.
In: Logic Colloquium 1973,
pp. 73–118.
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.
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.
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.
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.
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.
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.
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.
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.
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.
John C. Reynolds (1983):
Types, Abstraction and Parametric Polymorphism.
In: IFIP Congress,
pp. 513–523.
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.
Peter Selinger (2002):
The lambda calculus is algebraic.
J. Funct. Program. 12(6),
pp. 549–566,
doi:10.1017/S0956796801004294.
Aaron Stump (2017):
The calculus of dependent lambda eliminations.
Journal of Functional Programming 27,
pp. e14,
doi:10.1017/S0956796817000053.
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.
Aaron Stump & Peng Fu (2016):
Efficiency of lambda-encodings in total type theory.
Journal of Functional Programming 26,
doi:10.1017/S0956796816000034.
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.
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.