References

  1. A. Assaf (2015): A calculus of constructions with explicit subtyping. In: The 20th International Conference on Types for Proofs and Programs (TYPES '14).
  2. A. Assaf & G. Burel (2014): Translating HOL to Dedukti. Available at https://hal.archives-ouvertes.fr/hal-01097412.
  3. F. Blanqui (2015): Termination of rewrite relations on lambda-terms based on Girard's notion of reducibility.. Theoretical Computer Science. To appear.
  4. 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).
  5. M. Boespflug, Q. Carbonneaux, O. Hermant & R. Saillard: Dedukti. Available at http://dedukti.gforge.inria.fr.
  6. 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).
  7. R. Cauderlier & C. Dubois (2015): Objects and Subtyping in the λΠ-Calculus Modulo.
  8. 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.
  9. A. Dorra: Equivalence de Curry-Howard entre le lambda-Pi calcul et la logique intuitionniste. Report.
  10. 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.
  11. 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.
  12. 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.
  13. Aleksandar Nanevski, Frank Pfenning & Brigitte Pientka (2008): Contextual modal type theory. ACM Trans. Comput. Log. 9(3), doi:10.1145/1352582.1352591.
  14. 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.
  15. 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.
  16. 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.
  17. R. Saillard (2013): Towards explicit rewrite rules in the λΠ-calculus modulo. In: The 10th International Workshop on the Implementation of Logics (IWIL '13).

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