Mechanized Operational Semantics via (Co)Induction, TPHOLs'99, pp.221-238, 1999. ,
DOI : 10.1007/3-540-48256-3_15
URL : http://www.mcs.le.ac.uk/~sambler/papers/mosci98.ps.gz
Towards a Formally Verified Proof Assistant, ITP 2014, pp.27-44, 2014. ,
DOI : 10.1007/978-3-319-08970-6_3
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
De Bruijn Notation as a Nested Datatype, J. Funct. Program, vol.9, issue.1, pp.77-91, 1999. ,
The Locally Nameless Representation, Journal of Automated Reasoning, vol.40, issue.12, pp.363-408, 2012. ,
DOI : 10.1007/s10817-008-9097-2
TLC: A non-constructive library for Coq, 2017. ,
Mobile Processes: a Commented Bibliography, MOVEP'2K ? 4th Summer school on Modelling and Verification of Parallel processes, pp.206-222, 2001. ,
URL : https://hal.archives-ouvertes.fr/hal-01483577
Locally Nameless Permutation Types, 2012. ,
A Framework for the Formalisation of Pi Calculus Type Systems in Isabelle/HOL, pp.217-232, 2001. ,
DOI : 10.1007/3-540-44755-5_16
Bisimilarity as a Theory of Functional Programming, Electronic Notes in Theoretical Computer Science, vol.1, pp.232-252, 1995. ,
DOI : 10.1016/S1571-0661(04)80013-6
A Distribution Law for CCS and a New Congruence Result for the ??-Calculus, Lecture Notes in Computer Science), vol.4423, pp.228-242, 2007. ,
DOI : 10.1007/978-3-540-71389-0_17
URL : https://hal.archives-ouvertes.fr/hal-00089219
Proving Congruence of Bisimulation in Functional Programming Languages, Information and Computation, vol.124, issue.2, pp.103-112, 1996. ,
DOI : 10.1006/inco.1996.0008
Howe's Method for Contextual Semantics, 26th International Conference on Concurrency Theory, CONCUR 2015 (LIPIcs) Schloss Dagstuhl -Leibniz-Zentrum fuer Informatik, pp.212-225, 2015. ,
Characterizing contextual equivalence in calculi with passivation, Information and Computation, vol.209, issue.11, pp.1390-1433, 2011. ,
DOI : 10.1016/j.ic.2011.08.002
URL : https://hal.archives-ouvertes.fr/hal-00903877
HOCore in Coq, ITP 2015, pp.278-293, 2015. ,
DOI : 10.1007/978-3-319-22102-1_19
URL : https://hal.archives-ouvertes.fr/hal-01243017
A supposedly fun thing i may have to do again, Proceedings of the seventh international workshop on Logical frameworks and meta-languages, theory and practice, LFMTP '12, pp.33-42, 2012. ,
DOI : 10.1145/2364406.2364411
Higher-order psi-calculi, Mathematical Structures in Computer Science, vol.13, pp.1-37, 2014. ,
DOI : 10.1016/S0304-3975(00)00097-9
Proof-relevant ??-calculus: a constructive account of concurrency and causality, Mathematical Structures in Computer Science, vol.10, 2016. ,
DOI : 10.1016/0304-3975(89)90050-9
Higher-Order Abstract Syntax, PLDI 88, pp.199-208, 1988. ,
Nominal logic, a first order theory of names and binding, Information and Computation, vol.186, issue.2, pp.165-193, 2003. ,
DOI : 10.1016/S0890-5401(03)00138-X
Bisimulation for Higher-Order Process Calculi, Information and Computation, vol.131, issue.2, pp.141-178, 1996. ,
DOI : 10.1006/inco.1996.0096
URL : https://hal.archives-ouvertes.fr/inria-00074170
The Pi-Calculus: A Theory of Mobile Processes, 2001. ,
A Case-Study in Programming Coinductive Proofs: Howe's Method, 2016. ,