References

  1. M. Ashley-Rollman, K. Crary & R. Harper: A solution to the POPLmark Challenge.
  2. A. Avron, F. Honsell, I. A. Mason & R. Pollack (1992): Using Typed Lambda Calculus to Implement Formal Systems on a Machine. J. Autom. Reasoning 9(3), pp. 309–354. Available at http://dx.doi.org/10.1007/BF00245294.
  3. B. E. Aydemir et al. (2005): Mechanized Metatheory for the Masses: The PoplMark Challenge. In: Joe Hurd & Thomas F. Melham: TPHOLs, Lecture Notes in Computer Science 3603. Springer, pp. 50–65. Available at http://dx.doi.org/10.1007/11541868_4.
  4. B. E. Aydemir et al.: The POPLmark Challenge. Available at http://www.seas.upenn.edu/~plclub/poplmark/.
  5. A. Bucalo, F. Honsell, M. Miculan, I. Scagnetto & M. Hofmann (2006): Consistency of the theory of contexts. J. Funct. Program. 16(3), pp. 327–372. Available at http://dx.doi.org/10.1017/S0956796806005892.
  6. A. Charguéraud: A solution to the POPLmark Challenge.
  7. A. Charguéraud (2011): The Locally Nameless Representation. Journal of Automated Reasoning, pp. 1–46. Available at http://dx.doi.org/10.1007/s10817-011-9225-2.
  8. A. Chlipala: A solution to the POPLmark Challenge.
  9. A. Ciaffaglione, L. Liquori & M. Miculan (2003): Imperative Object-Based Calculi in Co-inductive Type Theories. In: Moshe Y. Vardi & Andrei Voronkov: LPAR, Lecture Notes in Computer Science 2850. Springer, pp. 59–77. Available at http://dx.doi.org/10.1007/978-3-540-39813-4_4.
  10. A. Ciaffaglione, L. Liquori & M. Miculan (2003): Reasoning on an imperative object-based calculus in Higher Order Abstract Syntax. In: MERLIN. ACM, pp. 1–10. Available at http://doi.acm.org/10.1145/976571.976574.
  11. A. Ciaffaglione, L. Liquori & M. Miculan (2007): Reasoning about Object-based Calculi in (Co)Inductive Type Theory and the Theory of Contexts. J. Autom. Reasoning 39(1), pp. 1–47. Available at http://dx.doi.org/10.1007/s10817-006-9061-y.
  12. A. Ciaffaglione & I. Scagnetto (2012): A solution to the POPLmark Challenge.
  13. T. Coquand & G. P. Huet (1988): The Calculus of Constructions. Inf. Comput. 76(2/3), pp. 95–120. Available at http://dx.doi.org/10.1016/0890-5401(88)90005-3.
  14. J. Despeyroux, A. P. Felty & A. Hirschowitz (1995): Higher-Order Abstract Syntax in Coq. In: Mariangiola Dezani-Ciancaglini & Gordon D. Plotkin: TLCA, Lecture Notes in Computer Science 902. Springer, pp. 124–138. Available at http://dx.doi.org/10.1007/BFb0014049.
  15. M. Fairbairn: A solution to the POPLmark Challenge.
  16. M. Gabbay & A. M. Pitts (2002): A New Approach to Abstract Syntax with Variable Binding. Formal Asp. Comput. 13(3-5), pp. 341–363. Available at http://dx.doi.org/10.1007/s001650200016.
  17. A. Gacek: A solution to the POPLmark Challenge.
  18. A. Gacek (2009): A Framework for Specifying, Prototyping, and Reasoning about Computational Systems. University of Minnesota.
  19. R. Harper, F. Honsell & G. D. Plotkin (1987): A Framework for Defining Logics. In: LICS. IEEE Computer Society, pp. 194–204.
  20. A. Hirschowitz & M. Maggesi: A solution to the POPLmark Challenge.
  21. A. Hirschowitz & M. Maggesi (2012): Nested Abstract Syntax in Coq. J. Autom. Reasoning 49(3), pp. 409–426. Available at http://dx.doi.org/10.1007/s10817-010-9207-9.
  22. M. Hofmann (1999): Semantical Analysis of Higher-Order Abstract Syntax. In: Proceedings of the 14th Annual IEEE Symposium on Logic in Computer Science, LICS '99. IEEE Computer Society, Washington, DC, USA, pp. 204–. Available at http://dl.acm.org/citation.cfm?id=788021.788940.
  23. F. Honsell, M. Miculan & I. Scagnetto (2001): An Axiomatic Approach to Metareasoning on Nominal Algebras in HOAS. In: Fernando Orejas, Paul G. Spirakis & Jan van Leeuwen: ICALP, Lecture Notes in Computer Science 2076. Springer, pp. 963–978. Available at http://dx.doi.org/10.1007/3-540-48224-5_78.
  24. F. Honsell, M. Miculan & I. Scagnetto (2001): pi-calculus in (Co)inductive-type theory. Theor. Comput. Sci. 253(2), pp. 239–285. Available at http://dx.doi.org/10.1016/S0304-3975(00)00095-5.
  25. F. Honsell, M. Miculan & I. Scagnetto (2001): The Theory of Contexts for First Order and Higher Order Abstract Syntax. Electr. Notes Theor. Comput. Sci. 62, pp. 116–135. Available at http://dx.doi.org/10.1016/S1571-0661(04)00323-8.
  26. X. Leroy: A solution to the POPLmark Challenge.
  27. X. Leroy (2007): A locally nameless solution to the POPLmark challenge. Research report 6098. INRIA.
  28. M. Miculan (1997): Encoding Logical Theories of Programs. Dipartimento di Informatica, Università di Pisa, Italy.
  29. M. Miculan, I. Scagnetto & F. Honsell (2005): Translating specifications from nominal logic to CIC with the theory of contexts. In: Randy Pollack: MERLIN. ACM, pp. 41–49. Available at http://doi.acm.org/10.1145/1088454.1088460.
  30. D. Miller & A. Tiu (2005): A proof theory for generic judgments. ACM Trans. Comput. Log. 6(4), pp. 749–783. Available at http://doi.acm.org/10.1145/1094622.1094628.
  31. C. Paulin-Mohring (1993): Inductive Definitions in the system Coq - Rules and Properties. In: Marc Bezem & Jan Friso Groote: TLCA, Lecture Notes in Computer Science 664. Springer, pp. 328–345. Available at http://dx.doi.org/10.1007/BFb0037116.
  32. F. Pfenning & C. Elliott (1988): Higher-Order Abstract Syntax. In: Richard L. Wexelblat: PLDI. ACM, pp. 199–208. Available at http://doi.acm.org/10.1145/53990.54010.
  33. B. C. Pierce (2002): Types and programming languages. MIT Press.
  34. A. M. Pitts (2003): Nominal logic, a first order theory of names and binding. Inf. Comput. 186(2), pp. 165–193. Available at http://dx.doi.org/10.1016/S0890-5401(03)00138-X.
  35. W. Ricciotti: A solution to the POPLmark Challenge.
  36. I. Scagnetto & M. Miculan (2002): Ambient Calculus and its Logic in the Calculus of Inductive Constructions. Electr. Notes Theor. Comput. Sci. 70(2), pp. 76–95. Available at http://dx.doi.org/10.1016/S1571-0661(04)80507-3.
  37. A. Stump: A solution to the POPLmark Challenge.
  38. The Coq Development Team (2011): The Coq Proof Assitant Reference Manual, version 8.3. INRIA. Available at http://coq.inria.fr/.
  39. C. Urban et al.: A solution to the POPLmark Challenge.
  40. H. Xi: A solution to the POPLmark Challenge.
Comments and questions to: eptcs@eptcs.org
For website issues: webmaster@eptcs.org