Mechanized operational semantics via (co)induction, TPHOLs'99, vol.1690, pp.221-238, 1999. ,
Towards a formally verified proof assistant, Lecture Notes in Computer Science, vol.8558, pp.27-44, 2014. ,
Mechanized metatheory for the masses: The PoplMark challenge, TPHOLs, pp.50-65, 2005. ,
LNgen: Tool support for locally nameless representations, 2010. ,
Abella: A system for reasoning about relational specifications, J. Formalized Reasoning, vol.7, issue.2, pp.1-89, 2014. ,
URL : https://hal.archives-ouvertes.fr/hal-01102709
Formalising the pi-calculus using nominal logic, Logical Methods in Computer Science, vol.5, issue.2, 2009. ,
De Bruijn notation as a nested datatype, J. Funct. Program, vol.9, issue.1, pp.77-91, 1999. ,
Consistency of the theory of contexts, J. Funct. Program, vol.16, issue.3, pp.327-372, 2006. ,
A linear logical framework, Inf. Comput, vol.179, issue.1, pp.19-75, 2002. ,
A concurrent logical framework ii: Examples and applications, 2002. ,
LN:locally nameless representation with cofinite quantification ,
TLC: A non-constructive library for Coq ,
The locally nameless representation, Journal of Automated Reasoning, vol.49, issue.3, pp.363-408, 2012. ,
Mechanizing type environments in weak, HOAS. Theor. Comput. Sci, vol.606, pp.57-78, 2015. ,
Mobile Processes: a Commented Bibliography. In MOVEP'2K -4th Summer school on Modelling and Verification of Parallel processes, Lecture Notes in Computer Science, vol.2067, pp.206-222, 2001. ,
URL : https://hal.archives-ouvertes.fr/hal-01483577
Lambda calculus notation with nameless dummies: A tool for automatic formula manipulation, with application to the church-rosser theorem, Indagationes Mathematicae, vol.75, issue.5, pp.381-392, 1972. ,
A higher-order specification of the pi-calculus, Lecture Notes in Computer Science, vol.1872, pp.425-439, 2000. ,
Higher-order abstract syntax in coq, TLCA '95, vol.902, pp.124-138, 1995. ,
URL : https://hal.archives-ouvertes.fr/inria-00074124
A framework for the formalisation of pi calculus type systems in Isabelle/HOL, vol.2152, pp.217-232, 2001. ,
Bisimilarity as a theory of functional programming, Electronic Notes in Theoretical Computer Science, vol.1, pp.232-252, 1995. ,
Proof of the subject reduction property for a pi-calculus in COQ, INRIA, 1999. ,
A full formalisation of pi-calculus theory in the calculus of constructions, Proceedings of the 10th International Conference on Theorem Proving in Higher Order Logics, vol.1275, pp.153-169, 1997. ,
Up to context proofs for the ?-calculus in the Coq system, 1997. ,
A distribution law for CCS and a new congruence result for the pi-calculus, Proc. of FoSSaCS'07, vol.4423, pp.228-242 ,
URL : https://hal.archives-ouvertes.fr/hal-00089219
, , 2007.
pi-calculus in (co)inductive-type theory, Theoretical Computer Science, vol.253, issue.2, pp.239-285, 2000. ,
The theory of contexts for first order and higher order abstract syntax, Electr. Notes Theor. Comput. Sci, vol.62, pp.116-135, 2001. ,
Proving congruence of bisimulation in functional programming languages. Information and Computation, vol.124, pp.103-112, 1996. ,
The pi-calculus in fm, Thirty Five Years of Automating Mathematics, vol.28, pp.247-269, 2003. ,
Needle & knot: Binder boilerplate tied up, ESOP 16, vol.9632, pp.419-445 ,
, , 2016.
Howe's method for contextual semantics, 26th International Conference on Concurrency Theory, vol.42, pp.212-225, 2015. ,
HO? in Coq, pp.252-265, 2018. ,
Characterizing contextual equivalence in calculi with passivation. Information and Computation, vol.209, pp.1390-1433, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00903877
Hocore in Coq, Lecture Notes in Computer Science, vol.9236, pp.278-293, 2015. ,
URL : https://hal.archives-ouvertes.fr/hal-01243017
Pure type systems formalized, TLCA '93, vol.664, pp.289-305, 1993. ,
A mechanized theory of the pi-calculus in HOL, Nord. J. Comput, vol.1, issue.1, pp.50-76, 1994. ,
A proof theory for generic judgments, ACM Trans. Comput. Log, vol.6, issue.4, pp.749-783, 2005. ,
A calculus of mobile processes, i. Information and Computation, vol.100, pp.1-40, 1992. ,
Mechanizing a pi-calculus equivalence in hol, TPHOL 95, pp.1-16, 1995. ,
A supposedly fun thing I may have to do again: a HOAS encoding of Howe's method, LFMTP 12, pp.33-42, 2012. ,
Higher-order psi-calculi, Mathematical Structures in Computer Science, vol.3, pp.1-37, 2014. ,
Proof-relevant ?-calculus: a constructive account of concurrency and causality, Mathematical Structures in Computer Science, vol.28, issue.9, pp.1541-1577, 2018. ,
Higher-order abstract syntax, PLDI 88, pp.199-208, 1988. ,
System description: Twelf -A meta-logical framework for deductive systems, Lecture Notes in Computer Science, vol.99, pp.202-206, 1999. ,
Beluga: A framework for programming and reasoning with deductive systems (system description), IJCAR 2010, vol.6173, pp.15-21, 2010. ,
Nominal logic, a first order theory of names and binding, Inf. Comput, vol.186, issue.2, pp.165-193, 2003. ,
A first-order syntax for the pi-calculus in isabelle/hol using permutations, Electr. Notes Theor. Comput. Sci, vol.58, issue.1, pp.1-17, 2001. ,
A fully adequate shallow embedding of the [pi]-calculus in isabelle/hol with mechanized syntax analysis, J. Funct. Program, vol.13, issue.2, pp.415-451, 2003. ,
Bisimulation for higher-order process calculi, vol.131, pp.141-178, 1996. ,
URL : https://hal.archives-ouvertes.fr/inria-00074170
The Pi-Calculus: A Theory of Mobile Processes, 2001. ,
Autosubst 2: reasoning with multi-sorted de bruijn terms and vector substitutions, CPP, vol.19, pp.166-180, 2019. ,
The Penn locally nameless metatheory library ,
A case-study in programming coinductive proofs: Howe's method. available at momigliano.di.unimi.it/papers/ bhowe.pdf, 2016. ,
Nominal techniques in Isabelle/HOL, J. Autom. Reasoning, vol.40, issue.4, pp.327-356, 2008. ,
Nominal 2. Archive of Formal Proofs, 2013. ,