A. Assaf (2015):
A calculus of constructions with explicit subtyping.
In: The 20th International Conference on Types for Proofs and Programs (TYPES '14).
F. Blanqui (2015):
Termination of rewrite relations on lambda-terms based on Girard's notion of reducibility..
Theoretical Computer Science.
To appear.
M. Boespflug & G. Burel (2012):
CoqInE : Translating the calculus of inductive constructions into the λΠ-calculus modulo..
In: The Second International Workshop on Proof Exchange for Theorem Proving (PxTP).
G. Burel (2013):
A Shallow Embedding of Resolution and Superposition Proofs into the λΠ-Calculus Modulo.
In: The Third International Workshop on Proof Exchange for Theorem Proving (PxTP '13).
R. Cauderlier & C. Dubois (2015):
Objects and Subtyping in the λΠ-Calculus Modulo.
D. Cousineau & G. Dowek (2007):
Embedding Pure Type Systems in λΠ-Calculus Modulo.
In: The 8th International Conference on Typed Lambda Calculi and Applications (TLCA '07),
doi:10.1007/978-3-540-73228-0_9.
A. Dorra:
Equivalence de Curry-Howard entre le lambda-Pi calcul et la logique intuitionniste.
Report.
H. Geuvers (1992):
The Church-Rosser Property for beta-eta-reduction in Typed lambda-Calculi.
In: The Seventh Annual Symposium on Logic in Computer Science (LICS '92),
doi:10.1109/LICS.1992.185556.
D. Miller (1991):
A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification.
Journal of Logic and Computation,
doi:10.1093/logcom/1.4.497.
F. Müller (1992):
Confluence of the Lambda Calculus with Left-Linear Algebraic Rewriting.
Information Processing Letters,
doi:10.1016/0020-0190(92)90155-O.
Aleksandar Nanevski, Frank Pfenning & Brigitte Pientka (2008):
Contextual modal type theory.
ACM Trans. Comput. Log. 9(3),
doi:10.1145/1352582.1352591.
T. Nipkow (1991):
Higher-Order Critical Pairs.
In: The Sixth Annual Symposium on Logic in Computer Science (LICS '91),
doi:10.1109/LICS.1991.151658.
V. van Oostrom (1995):
Development Closed Critical Pairs.
In: The Second International Workshop on Higher-Order Algebra, Logic, and Term Rewriting, (HOA '95),
doi:10.1007/3-540-61254-8_26.
Brigitte Pientka (2008):
A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions.
In: Symposium on Principles of Programming Languages, (POPL '08),
doi:10.1145/1328438.1328483.
R. Saillard (2013):
Towards explicit rewrite rules in the λΠ-calculus modulo.
In: The 10th International Workshop on the Implementation of Logics (IWIL '13).