A linear approach to the proof-theory of least and greatest fixed points, 2008. ,
Least and greatest fixed points in linear logic, ACM Trans. on Computational Logic, vol.13, issue.1, 2012. ,
The Bedwyr System for Model Checking over Syntactic Expressions, 21th Conf. on Automated Deduction (CADE), number 4603 in Lecture Notes in Artificial Intelligence, pp.391-397, 2007. ,
DOI : 10.1007/978-3-540-73595-3_28
Principles of Superdeduction, 22nd Annual IEEE Symposium on Logic in Computer Science (LICS 2007), pp.41-50, 2007. ,
DOI : 10.1109/LICS.2007.37
URL : https://hal.archives-ouvertes.fr/inria-00133557
Sequent calculi for induction and infinite descent, Journal of Logic and Computation, vol.21, issue.6, pp.1177-1216, 2011. ,
DOI : 10.1093/logcom/exq052
Subformula Linking as an Interaction Method, Proceedings of the 4th Conference on Interactive Theorem Proving (ITP), pp.386-401, 2013. ,
DOI : 10.1007/978-3-642-39634-2_28
URL : https://hal.archives-ouvertes.fr/hal-00937009
The Focused Calculus of Structures, Computer Science Logic: 20th Annual Conference of the EACSL, Leibniz International Proceedings in Informatics (LIPIcs) Schloss Dagstuhl?Leibniz-Zentrum für Informatik, pp.159-173, 2011. ,
URL : https://hal.archives-ouvertes.fr/hal-00772420
Theorem proving modulo, J. of Automated Reasoning, vol.31, issue.1, pp.31-72, 2003. ,
URL : https://hal.archives-ouvertes.fr/hal-01199506
A Two-Level Logic Approach to Reasoning About Computations, Journal of Automated Reasoning, vol.40, issue.4, pp.241-273, 2012. ,
DOI : 10.1007/s10817-011-9218-1
URL : https://hal.archives-ouvertes.fr/hal-00776208
Nested Deduction in Logical Foundations for Computation, 2013. ,
URL : https://hal.archives-ouvertes.fr/pastel-00929908
A proof calculus which reduces syntactic bureaucracy, Proceedings of the 21st International Conference on Rewriting Techniques and Applications of Leibniz International Proceedings in Informatics (LIPIcs) Schloss Dagstuhl?Leibniz-Zentrum fuer Informatik, pp.135-150, 2010. ,
URL : https://hal.archives-ouvertes.fr/hal-00529301
Handbook of Practical Logic and Automated Reasoning, 2009. ,
DOI : 10.1017/CBO9780511576430
Higher-order constraint simplification in dependent type theory, Proceedings of the Fourth International Workshop on Logical Frameworks and Meta-Languages Theory and Practice, LFMTP '09, pp.49-56, 2009. ,
DOI : 10.1145/1577824.1577832
Paramodulation and theorem-proving in first-order theories with equality, Machine Intelligence, vol.4, pp.135-150, 1969. ,
Rules of definitional reflection, [1993] Proceedings Eighth Annual IEEE Symposium on Logic in Computer Science, pp.222-232, 1993. ,
DOI : 10.1109/LICS.1993.287585
Linear Logic and Noncommutativity in the Calculus of Structures, 2003. ,
Some Observations on the Proof Theory of Second Order Propositional Multiplicative??Linear??Logic, Typed Lambda Calculi and Applications, TLCA'09, pp.309-324, 2009. ,
DOI : 10.1007/BF01622878
A Logical Framework for Reasoning about Logical Specifications, 2004. ,