, Mechanized metatheory for the masses: The POPLmark challenge, Theorem Proving in Higher Order Logics: 18th International Conference, number 3603 in Lecture Notes in Computer Science, pp.50-65, 2005.
, Abella: A system for reasoning about relational specifications, Journal of Formalized Reasoning, vol.7, issue.2, 2014.
URL : https://hal.archives-ouvertes.fr/hal-01102709
, Relating ?-calculus and ?-calculus by means of the linear substitution calculus, 2016.
, The locally nameless representation, Journal of Automated Reasoning, pp.1-46, 2011.
, Formalized meta-theory of sequent calculi for substructural logics, Workshop on Logical and Semantic Frameworks, with Applications (LSFA), 2016.
, A simpler proof theory for nominal logic, 8th International Conference on the Foundations of Software Science and Computational Structures (FOSSACS), vol.3441, pp.379-394, 2005.
, Parametric higher-order abstract syntax for mechanized semantics, Proceeding of the 13th ACM SIGPLAN international conference on Functional programming, pp.143-156, 2008.
, A verified compiler for an impure functional language, Proceedings of POPL'10, 2010.
, A formulation of the Simple Theory of Types, J. of Symbolic Logic, vol.5, pp.56-68, 1940.
, Hybrid: A definitional two-level approach to reasoning with higher-order abstract syntax, J. of Automated Reasoning, vol.48, pp.43-105, 2012.
, The Abella interactive theorem prover (system description), Fourth International Joint Conference on Automated Reasoning, vol.5195, pp.154-161, 2008.
, A Framework for Specifying, Prototyping, and Reasoning about Computational Systems, 2009.
, Nominal abstraction. Information and Computation, vol.209, pp.48-73, 2011.
DOI : 10.1016/j.ic.2010.09.004
URL : https://doi.org/10.1016/j.ic.2010.09.004
, A two-level logic approach to reasoning about computations, J. of Automated Reasoning, vol.49, issue.2, pp.241-273, 2012.
URL : https://hal.archives-ouvertes.fr/hal-00776208
, A framework for defining logics, Journal of the ACM, vol.40, issue.1, pp.143-184, 1993.
DOI : 10.1145/138027.138060
, Towards self-verification of HOL-Light, Proceedings of IJCAR'06, vol.4130, pp.177-191, 2006.
, An axiomatic approach to metareasoning on systems in higherorder abstract syntax, Proc. ICALP'01, number 2076 in Lecture Notes in Computer Science, pp.963-978, 2001.
, A logic programming language with lambda-abstraction, function variables, and simple unification, Extensions of Logic Programming: International Workshop, vol.475, pp.253-281, 1991.
DOI : 10.1007/bfb0038698
URL : https://repository.upenn.edu/cgi/viewcontent.cgi?article=1607&context=cis_reports
, Reasoning about computations using two-levels of logic, Proceedings of the 8th Asian Symposium on Programming Languages and Systems (APLAS'10), number 6461 in Lecture Notes in Computer Science, pp.34-46, 2010.
URL : https://hal.archives-ouvertes.fr/hal-00772599
, Programming with Higher-Order Logic, 2012.
DOI : 10.1017/cbo9781139021326
URL : https://hal.archives-ouvertes.fr/hal-00776197
, A supposedly fun thing I may have to do again: a HOAS encoding of Howe's method, Proceedings of LFMTP'12, pp.33-42, 2012.
, A case-study in programming coinductive proofs: Howe's method, 2017.
, Contextual model type theory, ACM Trans. on Computational Logic, vol.9, issue.3, pp.1-49, 2008.
DOI : 10.1145/1352582.1352591
, Logical frameworks, Handbook of Automated Reasoning (in 2 volumes), pp.1063-1147, 2001.
, Higher-order abstract syntax, Proceedings of the ACM-SIGPLAN Conference on Programming Language Design and Implementation, pp.199-208, 1988.
DOI : 10.1145/53990.54010
URL : http://www-2.cs.cmu.edu/~fp/papers/pldi88.pdf
, A type-theoretic foundation for programming with higher-order abstract syntax and first-class substitutions, 35th Annual ACM Symposium on Principles of Programming Languages (POPL'08), pp.371-382, 2008.
DOI : 10.1145/1328897.1328483
, Beluga: A framework for programming and reasoning with deductive systems (system description), Fifth International Joint Conference on Automated Reasoning, number 6173 in Lecture Notes in Computer Science, pp.15-21, 2010.
DOI : 10.1007/978-3-642-14203-1_2
URL : http://www.cs.mcgill.ca/~complogic/beluga/submitted/system-description.pdf
, Nominal logic, A first order theory of names and binding. Information and Computation, vol.186, pp.165-193, 2003.
, Howe's method for higher-order languages, Advanced Topics in Bisimulation and Coinduction, pp.197-232, 2011.
, Automatically deriving schematic theorems for dynamic contexts, International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2014.
, The lambda sigma calculus and strong normalization, 2011.
, Autosubst: Reasoning with de Bruijn terms and parallel substitutions, Proceedings of ITP'15, 2015.
, Rules of definitional reflection, 8th Symp. on Logic in Computer Science, pp.222-232, 1993.
, Nominal reasoning techniques in Isabelle/HOL, Journal of Automated Reasoning, vol.40, issue.4, pp.327-356, 2008.
, Nominal techniques in Isabelle/HOL, 20th Conf. on Automated Deduction, vol.3632, pp.38-53, 2005.
, Reasoning about higher-order relational specifications, Proceedings of the 15th International Symposium on Princples and Practice of Declarative Programming (PPDP), pp.157-168, 2013.
DOI : 10.1145/2505879.2505889
URL : https://hal.archives-ouvertes.fr/hal-00787126