CSDAI

 Department of Institut Polytechnique de Paris

Group partout

partout (Proof Automation and RepresenTation: a fOundation of compUtation and deducTion)

LIX, Ecole Polytechnique

Themes:foundations of computer science

The PARTOUT project is interested in the principles of deductive and computational formalisms. In the broadest sense, we are interested in the question of trustworthy and verifiable meta-theory.

Contact person: luts Strassburger, http://www.lix.polytechnique.fr/~lutz

Web site: https://team.inria.fr/partout/

Journal articles

2025

ref_biblio
Clément Allain, Frédéric Bour, Basile Clément, François Pottier, Gabriel Scherer. Tail Modulo Cons, OCaml, and Relational Separation Logic. Proceedings of the ACM on Programming Languages, 2025, 9 (POPL), pp.2337-2363. ⟨10.1145/3704915⟩. ⟨hal-04884634⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04884634/file/tmc-popl2025.pdf BibTex
ref_biblio
Paul-André Melliès, Noam Zeilberger. The categorical contours of the Chomsky-Schützenberger representation theorem. Logical Methods in Computer Science, 2025, Volume 21, Issue 2, ⟨10.46298/lmcs-21(2:12)2025⟩. ⟨hal-04399404v2⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04399404/file/2405.14703.pdf BibTex

2024

ref_biblio
Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni. Reasonable Space for the Lambda-Calculus, Logarithmically. Logical Methods in Computer Science, 2024, 20 (4), ⟨10.46298/lmcs-20(4:15)2024⟩. ⟨hal-04835903⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04835903/file/lmcs2024.pdf BibTex
ref_biblio
Bryce Clarke. Lifting twisted coreflections against delta lenses. Theory and Applications of Categories, 2024, 41 (26), pp.838-877. ⟨hal-04430822v2⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04430822/file/2401.17250v2.pdf BibTex
ref_biblio
Pablo Donato. The Flower Calculus. Leibniz International Proceedings in Informatics , 2024, 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024) (299), pp.5:1-5:24. ⟨hal-04472717v3⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04472717/file/full.pdf BibTex
ref_biblio
André Hirschowitz, Tom Hirschowitz, Ambroise Lafont, Marco Maggesi. Variable binding and substitution for (nameless) dummies. Logical Methods in Computer Science, 2024, 20 (1), ⟨10.46298/lmcs-20(1:18)2024⟩. ⟨hal-04487704⟩
Accès au bibtex
https://arxiv.org/pdf/2209.02614 BibTex
ref_biblio
Dale Miller, Alberto Momigliano. Property-Based Testing by Elaborating Proof Outlines. Theory and Practice of Logic Programming, In press. ⟨hal-04710992⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04710992/file/pbt-final.pdf BibTex

2023

ref_biblio
Beniamino Accattoli. Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic. Logical Methods in Computer Science, 2023, Volume 19, Issue 4, ⟨10.46298/lmcs-19(4:23)2023⟩. ⟨hal-04374165⟩
Accès au bibtex
https://arxiv.org/pdf/2205.15203 BibTex
ref_biblio
Lê Thành Dũng Nguyên, Lutz Straßburger. A System of Interaction and Structure III: The Complexity of BV and Pomset Logic. Logical Methods in Computer Science, 2023, 9 (4), ⟨10.46298/LMCS-19(4:25)2023⟩. ⟨hal-03909547v2⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03909547/file/2209.07825.pdf BibTex
ref_biblio
Wendlasida Ouedraogo, Lutz Strassburger, Gabriel Scherer. Coqlex: Generating Formally Verified Lexers. The Art, Science, and Engineering of Programming, 2023, 8 (1), ⟨10.22152/programming-journal.org/2024/8/3⟩. ⟨hal-03912170v2⟩
Accès au texte intégral et bibtex
https://hal.science/hal-03912170/file/2306.12411.pdf BibTex

2022

ref_biblio
Beniamino Accattoli, Giulio Guerrieri. The theory of call-by-value solvability. Proceedings of the ACM on Programming Languages, 2022, 6 (ICFP), pp.855-885. ⟨10.1145/3547652⟩. ⟨hal-03912446⟩
Accès au bibtex
BibTex
ref_biblio
Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni. Multi Types and Reasonable Space. Proceedings of the ACM on Programming Languages, 2022, 6 (ICFP), pp.799-825. ⟨10.1145/3547650⟩. ⟨hal-03912436⟩
Accès au bibtex
BibTex
ref_biblio
Matteo Acclavio, Ross Horne, Lutz Strassburger. An Analytic Propositional Proof System On Graphs. Logical Methods in Computer Science, 2022, 18 (4), ⟨10.46298/LMCS-18(4:1)2022⟩. ⟨hal-03087392v2⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03087392/file/LBF-LMCS.pdf BibTex
ref_biblio
Nathanaëlle Courant, Julien Lepiller, Gabriel Scherer. Debootstrapping without Archeology. The Art, Science, and Engineering of Programming, 2022, 6 (3), ⟨10.22152/programming-journal.org/2022/6/13⟩. ⟨hal-03917754⟩
Accès au texte intégral et bibtex
https://hal.science/hal-03917754/file/camlboot.pdf BibTex
ref_biblio
Sonia Marin, Dale Miller, Elaine Pimentel, Marco Volpe. From axioms to synthetic inference rules via focusing. Annals of Pure and Applied Logic, 2022, 173 (5), pp.103091. ⟨10.1016/j.apal.2022.103091⟩. ⟨hal-03792129⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03792129/file/synthetic-rules-via-focusing.pdf BibTex
ref_biblio
Dale Miller. A Survey of the Proof-Theoretic Foundations of Logic Programming. Theory and Practice of Logic Programming, 2022, 22 (6), pp.859 - 904. ⟨10.1017/S1471068421000533⟩. ⟨hal-03411144⟩
Accès au bibtex
https://arxiv.org/pdf/2109.01483 BibTex

2021

ref_biblio
Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni. The (In)Efficiency of interaction. Proceedings of the ACM on Programming Languages, 2021, 5 (POPL), pp.1-33. ⟨10.1145/3434332⟩. ⟨hal-03346750⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03346750/file/2010.12988.pdf BibTex
ref_biblio
Marianna Girlando, Sara Negri, Nicola Olivetti. Uniform labelled calculi for preferential conditional logics based on neighbourhood semantics. Journal of Logic and Computation, 2021, 31 (3), pp.947-997. ⟨10.1093/logcom/exab019⟩. ⟨hal-02330319v3⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02330319/file/girlando_negri_olivetti_JLC2021.pdf BibTex
ref_biblio
Tomer Libal, Dale Miller. Functions-as-constructors higher-order unification: extended pattern unification. Annals of Mathematics and Artificial Intelligence, 2021, ⟨10.1007/s10472-021-09774-y⟩. ⟨hal-03457303⟩
Accès au bibtex
BibTex
ref_biblio
Sonia Marin, Marianela Morales, Lutz Strassburger. A fully labelled proof system for intuitionistic modal logics. Journal of Logic and Computation, 2021, 31 (3), pp.998-1022. ⟨10.1093/logcom/exab020⟩. ⟨hal-02390454v3⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02390454/file/document.pdf BibTex
ref_biblio
Dale Miller. Reciprocal Influences Between Proof Theory and Logic Programming. Philosophy & Technology, 2021, 34, pp.75-104. ⟨10.1007/s13347-019-00370-x⟩. ⟨hal-02368867⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02368867/file/lppt-extended.pdf BibTex
ref_biblio
Dale Miller, Alexandre Viel. The undecidability of proof search when equality is a logical connective. Annals of Mathematics and Artificial Intelligence, 2021, ⟨10.1007/s10472-021-09764-0⟩. ⟨hal-03457312⟩
Accès au texte intégral et bibtex
https://hal.science/hal-03457312/file/ps-equality.pdf BibTex
ref_biblio
Alban Reynaud, Gabriel Scherer, Jeremy Yallop. A practical mode system for recursive definitions. Proceedings of the ACM on Programming Languages, 2021, 5 (POPL), pp.1-29. ⟨10.1145/3434326⟩. ⟨hal-03125031⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03125031/file/letrec.pdf BibTex

2020

ref_biblio
Beniamino Accattoli, Stéphane Graham-Lengrand, Delia Kesner. Tight typings and split bounds, fully developed. Journal of Functional Programming, 2020, 30, ⟨10.1017/S095679682000012X⟩. ⟨hal-03089347⟩
Accès au bibtex
BibTex

2019

ref_biblio
Beniamino Accattoli, Giulio Guerrieri. Abstract Machines for Open Call-by-Value. Science of Computer Programming, 2019, 184, ⟨10.1016/j.scico.2019.03.002⟩. ⟨hal-02415780⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02415780/file/1-s2.0-S016764231830042X-main.pdf BibTex
ref_biblio
Kaustuv Chaudhuri, Leonardo Lima, Giselle Reis. Formalized meta-theory of sequent calculi for linear logics. Theoretical Computer Science, 2019, 781, pp.24-38. ⟨10.1016/j.tcs.2019.02.023⟩. ⟨hal-04318000⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04318000/file/cut-elim-abella.pdf BibTex
ref_biblio
Kaustuv Chaudhuri, Carlos Olarte, Elaine Pimentel, Joëlle Despeyroux. Hybrid Linear Logic, revisited. Mathematical Structures in Computer Science, In press, ⟨10.1017/S0960129518000439⟩. ⟨hal-01968154⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01968154/file/MSCS_HAL.pdf BibTex
ref_biblio
Julien Courtiel, Karen Yeats, Noam Zeilberger. Connected chord diagrams and bridgeless maps. The Electronic Journal of Combinatorics, 2019, 26 (4), pp.1-56. ⟨10.37236/7400⟩. ⟨hal-01650141v2⟩
Accès au texte intégral et bibtex
https://hal.science/hal-01650141/file/CoYeZe-final.pdf BibTex
ref_biblio
Quentin Heath, Dale Miller. A proof theory for model checking. Journal of Automated Reasoning, 2019, 63 (4), pp.857-885. ⟨10.1007/s10817-018-9475-3⟩. ⟨hal-01814006⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01814006/file/hal.pdf BibTex
ref_biblio
Roman Kuznets, Lutz Strassburger. Maehara-style modal nested calculi. Archive for Mathematical Logic, 2019, 58 (3-4), pp.359-385. ⟨10.1007/s00153-018-0636-1⟩. ⟨hal-01942240⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01942240/file/10.1007%252Fs00153-018-0636-1.pdf BibTex
ref_biblio
Dale Miller. Mechanized metatheory revisited. Journal of Automated Reasoning, 2019, 63 (3), pp.625-665. ⟨10.1007/s10817-018-9483-3⟩. ⟨hal-01884210⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01884210/file/paper.pdf BibTex
ref_biblio
Lutz Strassburger. Deep inference and expansion trees for second-order multiplicative linear logic. Mathematical Structures in Computer Science, 2019, Special Issue 8 (A special issue on structural proof theory, automated reasoning and computation in celebration of Dale Miller’s 60th birthday), 29, pp.1030-1060. ⟨10.1017/S0960129518000385⟩. ⟨hal-01942410⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01942410/file/ExpTreesLL.pdf BibTex
ref_biblio
Lutz Strassburger. On the decision problem for MELL. Theoretical Computer Science, 2019, 768, pp.91-98. ⟨10.1016/j.tcs.2019.02.022⟩. ⟨hal-02386746⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02386746/file/OnDeciMELL.pdf BibTex
ref_biblio
Lutz Strassburger. The problem of proof identity, and why computer scientists should care about Hilbert's 24th problem. Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, 2019, 377 (2140), pp.20180038. ⟨10.1098/rsta.2018.0038⟩. ⟨hal-02475417⟩
Accès au bibtex
BibTex
ref_biblio
Noam Zeilberger. A sequent calculus for a semi-associative law. Logical Methods in Computer Science, 2019, 15 (1), pp.1-23. ⟨10.23638/LMCS-15(1:9)2019⟩. ⟨hal-03131847⟩
Accès au bibtex
https://arxiv.org/pdf/1803.10080 BibTex

Conference papers

2025

ref_biblio
Victoria Barrett, Alessio Guglielmi, Benjamin Ralph. A strictly linear subatomic proof system. CSL 2025 - 33rd EACSL Annual Conference on Computer Science Logic, Feb 2025, Amsterdam, Netherlands. ⟨hal-04845619⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04845619/file/slsps.pdf BibTex
ref_biblio
Dale Miller. Linear logic using negative connectives: extended version. FSCD 2025 - 10th International Conference on Formal Structures for Computation and Deduction, Jul 2025, Birmingham, United Kingdom. pp.26:1-26:26, ⟨10.4230/LIPIcs.FSCD.2025.26⟩. ⟨hal-05067259⟩
Accès au texte intégral et bibtex
https://hal.science/hal-05067259/file/root.pdf BibTex

2024

ref_biblio
Beniamino Accattoli, Jui-Hsuan Wu. Positive Focusing is Directly Useful. MFPS 2024 - 40th Conference on Mathematical Foundations of Programming Semantics, Jun 2024, Oxford, United Kingdom. ⟨10.46298/entics.14758⟩. ⟨hal-04886376⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04886376/file/2411.09489%20%281%29.pdf BibTex
ref_biblio
Beniamino Accattoli, Adrienne Lancelot. Mirroring Call-By-Need, or Values Acting Silly. FSCD 2024 - 9th International Conference on Formal Structures for Computation and Deduction, Jul 2024, Tallin, Estonia. ⟨10.4230/LIPIcs.FSCD.2024.23⟩. ⟨hal-04837722⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04837722/file/LIPIcs.FSCD.2024.23.pdf BibTex
ref_biblio
Beniamino Accattoli. Semantic Bounds and Multi Types, Revisited. CSL 2024 - 32nd EACSL Annual Conference on Computer Science Logic, Feb 2024, Naples, Italy. ⟨10.4230/LIPIcs.CSL.2024.7⟩. ⟨hal-04837714⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04837714/file/LIPIcs.CSL.2024.7.pdf BibTex
ref_biblio
Beniamino Accattoli, Adrienne Lancelot. Light Genericity. FoSSaCS 2024 - 27th International Conference on Foundations of Software Science and Computation Structures, Apr 2024, Luxembourg City, Luxembourg. pp.24-46, ⟨10.1007/978-3-031-57231-9_2⟩. ⟨hal-04886354⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04886354/file/978-3-031-57231-9_2%20%281%29.pdf BibTex
ref_biblio
Beniamino Accattoli, Claudio Sacerdoti Coen. IMELL Cut Elimination with Linear Overhead. 9th International Conference on Formal Structures for Computation and Deduction (FSCD 2024), Jul 2024, Tallin, Estonia. ⟨10.4230/LIPICS.FSCD.2024.24⟩. ⟨hal-04837719⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04837719/file/LIPIcs.FSCD.2024.24.pdf BibTex
ref_biblio
Clément Allain, Gabriel Scherer. Correct tout seul, sûr à plusieurs. 35es Journées Francophones des Langages Applicatifs (JFLA 2024), Jan 2024, Saint-Jacut-de-la-Mer, France. ⟨hal-04406412⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04406412/file/jfla2024-paper-29.pdf BibTex
ref_biblio
Marianna Girlando, Roman Kuznets, Sonia Marin, Marianela Morales, Lutz Straßburger. A Simple Loopcheck for Intuitionistic K. Logic, Language, Information, and Computation. WoLLIC 2024, Jun 2024, Bern, Switzerland, Switzerland. pp.47-63, ⟨10.1007/978-3-031-62687-6_4⟩. ⟨hal-04569308⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04569308/file/main-nocomment.pdf BibTex
ref_biblio
Ambroise Lafont. A diagram editor to mechanise categorical proofs. JFLA 2024 - 35es Journées Francophones des Langages Applicatifs, Jan 2024, Saint-Jacut-de-la-Mer, France. ⟨hal-04407118⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04407118/file/jfla2024-paper-53.pdf BibTex
ref_biblio
Mehrnoosh Sadrzadeh, Lutz Straßburger. Lambek Calculus with Banged Atoms for Parasitic Gaps. Logic, Language, Information, and Computation. WoLLIC 2024, Jun 2024, Bern, Switzerland. pp.193-209, ⟨10.1007/978-3-031-62687-6_13⟩. ⟨hal-04569184⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04569184/file/main-final.pdf BibTex

2023

ref_biblio
Beniamino Accattoli, Pablo Barenbaum. A Diamond Machine for Strong Evaluation. APLAS 2023 - The 21st Asian Symposium on Programming Languages and Systems, Nov 2023, Taipei, Taiwan. ⟨hal-04395635⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04395635/file/main.pdf BibTex
ref_biblio
Beniamino Accattoli, Horace Blanc, Claudio Sacerdoti Coen. Formalizing Functions as Processes. ITP 2023 - 14th International Conference on Interactive Theorem Proving, Jul 2023, Bialystok, Poland. ⟨10.4230/LIPICS.ITP.2023.5⟩. ⟨hal-04280546⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04280546/file/LIPIcs.ITP.2023.5.pdf BibTex
ref_biblio
Beniamino Accattoli. Sharing a Perspective on the lambda Calculus. Onward! 2023 - ACM SIGPLAN International Symposium on New Ideas, New Paradigms, and Reflections on Programming and Software, Oct 2023, Cascais, Portugal. pp.179-190, ⟨10.1145/3622758.3622884⟩. ⟨hal-04280550⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04280550/file/3622758.3622884.pdf BibTex
ref_biblio
Beniamino Accattoli, Giulio Guerrieri, Maico Leberle. Strong Call-by-Value and Multi Types. ICTAC 2023 - 20th International Colloquium on Theoretical Aspects of Computing, Dec 2023, Lima, Peru. ⟨hal-04395549⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04395549/file/main.pdf BibTex
ref_biblio
Farah Al Wardani, Kaustuv Chaudhuri, Dale Miller. Formal Reasoning using Distributed Assertions. FroCoS 2023 - 14th International Symposium on Frontiers of Combining Systems, Sep 2023, Prague (Czech Republic), Czech Republic. ⟨hal-04167922v2⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04167922/file/damf.pdf BibTex
ref_biblio
Nicolas Behr, Paul-André Melliès, Noam Zeilberger. Convolution Products on Double Categories and Categorification of Rule Algebras. FSCD 2023 - 8th International Conference on Formal Structures for Computation and Deduction, Jul 2023, Rome, Italy. pp.17:1-17:20, ⟨10.4230/LIPIcs.FSCD.2023.17⟩. ⟨hal-04222049⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04222049/file/LIPIcs.FSCD.2023.17.pdf BibTex
ref_biblio
Bryce Clarke. The Algebraic Weak Factorisation System for Delta Lenses. Proceedings of the Sixth International Conference on Applied Category Theory 2023, Jul 2023, University of Maryland, College Park, MD, United States. pp.54-69, ⟨10.4204/EPTCS.397.4⟩. ⟨hal-04089742v2⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04089742/file/The-awfs-for-delta-lenses.pdf BibTex
ref_biblio
Marianna Girlando, Roman Kuznets, Sonia Marin, Marianela Morales, Lutz Strassburger. Intuitionistic S4 is decidable. LICS 2023- 38th Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2023, Boston, United States. pp.1-13, ⟨10.1109/LICS56636.2023.10175684⟩. ⟨hal-04267899⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04267899/file/2304.12094.pdf BibTex
ref_biblio
Dale Miller. A system of inference based on proof search: an extended abstract. LICS 2023 - 38th Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2023, Boston, United States. pp.1-11, ⟨10.1109/LICS56636.2023.10175827⟩. ⟨hal-04169014v2⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04169014/file/lics2023.pdf BibTex
ref_biblio
Dale Miller, Jui-Hsuan Wu. A positive perspective on term representation: Extended paper. CSL 2023 - Computer Science Logic, Feb 2023, Warsaw, Poland. ⟨hal-03843587v2⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03843587/file/csl2023-techrep.pdf BibTex
ref_biblio
Camille Noûs, Gabriel Scherer. Backtracking reference stores. JFLA 2023 - 34èmes Journées Francophones des Langages Applicatifs, Jan 2023, Praz-sur-Arly, France. pp.190-210. ⟨hal-03936704⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03936704/file/jfla23_paper_9677.pdf BibTex
ref_biblio
Jui-Hsuan Wu. Proofs as Terms, Terms as Graphs. APLAS 2023 - 21st Asian Symposium on Programming Languages and Systems, Nov 2023, Taipei, Taiwan. ⟨hal-04222527⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04222527/file/APLAS_full.pdf BibTex

2022

ref_biblio
Beniamino Accattoli. Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic. LICS 2022 - 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Aug 2022, Haifa, Israel. pp.1-15, ⟨10.1145/3531130.3532445⟩. ⟨hal-03912448⟩
Accès au bibtex
https://arxiv.org/pdf/2205.15203 BibTex
ref_biblio
Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni. Reasonable Space for the λ-Calculus, Logarithmically. LICS 2022 - 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Aug 2022, Haifa, Israel. pp.1-13, ⟨10.1145/3531130.3533362⟩. ⟨hal-03912449⟩
Accès au bibtex
BibTex
ref_biblio
Beniamino Accattoli, Maico Leberle. Useful Open Call-By-Need. CSL 2022 - 30th EACSL Annual Conference on Computer Science Logic, Feb 2022, Gottingen, Germany. ⟨10.4230/LIPIcs.CSL.2022.4⟩. ⟨hal-03912452⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03912452/file/LIPIcs-CSL-2022-4.pdf BibTex
ref_biblio
Matteo Acclavio, Ross Horne, Sjouke Mauw, Lutz Straßburger. A Graphical Proof Theory of Logical Time. FSCD 2022 - 7th International Conference on Formal Structures for Computation and Deduction, Aug 2022, Haifa, Israel. ⟨10.4230/LIPIcs.FSCD.2022.22⟩. ⟨hal-03909486⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03909486/file/LIPIcs-FSCD-2022-22.pdf BibTex
ref_biblio
Matteo Acclavio, Lutz Straßburger. Combinatorial Proofs for Constructive Modal Logic. AiML 2022 - Advances in Modal Logic, Aug 2022, Rennes, France. ⟨hal-03909538⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03909538/file/AiML2022.pdf BibTex
ref_biblio
Nicolas Chataing, Camille Noûs, Gabriel Scherer. Déboîter les constructeurs. Journées Francophones des Langages Applicatifs, Feb 2022, Saint-Médard-d'Excideuil, France. ⟨hal-03510931⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03510931/file/paper.pdf BibTex
ref_biblio
Agata Ciabattoni, Lutz Straßburger, Matteo Tesi. Taming Bounded Depth with Nested Sequents. AIML 2022 - Advances in Modal Logic, Aug 2022, Rennes, France. ⟨hal-03909534⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03909534/file/main.pdf BibTex
ref_biblio
Pablo Donato, Pierre-Yves Strub, Benjamin Werner. A drag-and-drop proof tactic. CPP 2022: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2022, Philadelphia, United States. pp.197-209, ⟨10.1145/3497775.3503692⟩. ⟨hal-03823357v2⟩
Accès au texte intégral et bibtex
https://hal.science/hal-03823357/file/cpp-article.pdf BibTex
ref_biblio
Pablo Donato, Pierre-Yves Strub, Benjamin Werner. Actema : une interface graphique et gestuelle pour preuves formelles (démonstration). 33èmes Journées Francophones des Langages Applicatifs, Jun 2022, Saint-Médard-d'Excideuil, France. pp.267-268. ⟨hal-03626854⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03626854/file/jfla22_paper_26.pdf BibTex
ref_biblio
Willem Heijltjes, Dominic Hughes, Lutz Strassburger. Normalization Without Syntax. FSCD 2022, Aug 2022, Haifa, Israel. ⟨hal-03654060⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03654060/file/FSCD2022_paper_1156.pdf BibTex
ref_biblio
Paul-André Melliès, Noam Zeilberger. Parsing as a lifting problem and the Chomsky-Schützenberger representation theorem. MFPS 2022 - 38th conference on Mathematical Foundations for Programming Semantics, Jul 2022, Ithaca, NY, United States. ⟨10.46298/entics.10508⟩. ⟨hal-03702762⟩
Accès au texte intégral et bibtex
https://hal.science/hal-03702762/file/paper-mfps.pdf BibTex
ref_biblio
Guillaume Munch-Maccagnoni, Gabriel Scherer. Boxroot, fast movable GC roots for a better FFI. ML Family Workshop, Benoît Montagu, Sep 2022, Ljubljana, Slovenia. ⟨hal-03910313⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03910313/file/boxroot-mlworkshop.pdf BibTex
ref_biblio
Lê Thành Dung Nguyên, Lutz Straßburger. BV and Pomset Logic Are Not the Same. CSL 2022 - 30th EACSL Annual Conference on Computer Science Logic, Feb 2022, Göttingen, Germany. ⟨10.4230/LIPIcs.CSL.2022.32⟩. ⟨hal-03909463⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03909463/file/LIPIcs-CSL-2022-32.pdf BibTex
ref_biblio
Giti Omidvar, Lutz Straßburger. Combinatorial Flows as Bicolored Atomic Flows. WoLLIC 2022 - 28th Workshop on Logic, Language, Information and Computation, Sep 2022, Iaşi, Romania. pp.141-157, ⟨10.1007/978-3-031-15298-6_9⟩. ⟨hal-03909530⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03909530/file/Combinatorial_Flows.pdf BibTex
ref_biblio
Gabriel Scherer, Nathanaëlle Courant. An OCaml use case for strong call-by-need reduction. ACM SIGPLAN Workshop on ML 2022 - ML Family Workshop, Benoit Montagu, Sep 2022, Ljubljana, Slovenia. ⟨hal-03947986⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03947986/file/shapes-workshop.pdf BibTex

2021

ref_biblio
Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni. The Space of Interaction. LICS 2021 - 36th Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2021, Rome, France. pp.1-13, ⟨10.1109/LICS52264.2021.9470726⟩. ⟨hal-03346767⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03346767/file/2104.13795.pdf BibTex
ref_biblio
Beniamino Accattoli, Claudia Faggian, Giulio Guerrieri. Factorize Factorization. CSL 2021 - 29th EACSL Annual Conference on Computer Science Logic, Jan 2021, Ljubljana, Slovenia. ⟨10.4230/LIPIcs.CSL.2021.22⟩. ⟨hal-03044338⟩
Accès au texte intégral et bibtex
https://hal.science/hal-03044338/file/main_modular.pdf BibTex
ref_biblio
Beniamino Accattoli, Andrea Condoluci, Claudio Sacerdoti Coen. Strong Call-by-Value is Reasonable, Implosively. 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jun 2021, Rome, Italy. pp.1-14, ⟨10.1109/LICS52264.2021.9470630⟩. ⟨hal-03475461⟩
Accès au bibtex
BibTex
ref_biblio
Matteo Acclavio, Davide Catta, Lutz Strassburger. Game Semantics for Constructive Modal Logic. TABLEAUX 2021 - 30th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Sep 2021, Birmingham, United Kingdom. pp.428-445, ⟨10.1007/978-3-030-86059-2_25⟩. ⟨hal-03369819⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03369819/file/Tableaux2021-Paper27.pdf BibTex
ref_biblio
Frédéric Bour, Basile Clément, Gabriel Scherer. Tail Modulo Cons. JFLA 2021 - Journées Francophones des Langages Applicatifs, Apr 2021, Saint Médard d’Excideuil, France. ⟨hal-03146495⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03146495/file/tmc.pdf BibTex
ref_biblio
Nicolas Chataing, Gabriel Scherer. Unfolding ML datatype declarations without loops. ML Family Workshop, Aug 2021, online, South Korea. ⟨hal-03510898⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03510898/file/constructor-unboxing-ml-workshop-2021.pdf BibTex
ref_biblio
Kaustuv Chaudhuri. Subformula Linking for Intuitionistic Logic with Application to Type Theory. CADE 2021 - 28th International Conference on Automated Deduction, Jul 2021, Pittsburgh, PA (Virtual), United States. pp.200-216, ⟨10.1007/978-3-030-79876-5_12⟩. ⟨hal-03528659⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03528659/file/paper39_hal.pdf BibTex
ref_biblio
Dominic J D Hughes, Lutz Strassburger, Jui-Hsuan Wu. Combinatorial Proofs and Decomposition Theorems for First-order Logic. 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jun 2021, Rome, Italy. pp.1-13, ⟨10.1109/LICS52264.2021.9470579⟩. ⟨hal-03369764⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03369764/file/2104.13124.pdf BibTex
ref_biblio
Olivier Martinot, Gabriel Scherer. Frozen inference constraints for type-directed disambiguation. ML Family Workshop, Aug 2021, online, South Korea. ⟨hal-03510890⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03510890/file/short-abstract.pdf BibTex
ref_biblio
Wendlasida Ouedraogo, Danko Ilik, Lutz Strassburger. Demo Paper: Coqlex, an approach to generate verified lexers. ML 2021-ACM SIGPLAN Workshop on ML, Aug 2021, Online event, United States. ⟨hal-03470713⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03470713/file/Demo_Paper.pdf BibTex

2020

ref_biblio
Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni. The Machinery of Interaction. PPDP '20 - 22nd International Symposium on Principles and Practice of Declarative Programming, Sep 2020, Bologna, Italy. pp.1-15, ⟨10.1145/3414080.3414108⟩. ⟨hal-03089342⟩
Accès au bibtex
BibTex
ref_biblio
Beniamino Accattoli, Alejandro Díaz-Caro. Functional Pearl: The Distributive $\lambda$-Calculus. FLOPS 2020 - 15th International Symposium on Functional and Logic Programming, Sep 2020, Akita, Japan. pp.33-49, ⟨10.1007/978-3-030-59025-3_3⟩. ⟨hal-03089254⟩
Accès au bibtex
BibTex
ref_biblio
Matteo Acclavio, Ross Horne, Lutz Strassburger. Logic beyond formulas: a proof system on graphs. LICS 2020 - 35th ACM/IEEE Symposium on Logic in Computer Science, Jul 2020, Saarbrücken, Germany. pp.38-52, ⟨10.1145/3373718.3394763⟩. ⟨hal-02560105⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02560105/file/LBF.pdf BibTex
ref_biblio
Matteo Acclavio, Roberto Maieli. Generalized connectives for multiplicative linear logic. CSL 2020 - 28th EACSL annual conference on Computer Science Logic, Jan 2020, Barcelona, Spain. pp.6:1-6:15, ⟨10.4230/LIPIcs.CSL.2020.6⟩. ⟨hal-02492258⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02492258/file/LIPIcs-CSL-2020-6.pdf BibTex
ref_biblio
Nicolas Blanco, Noam Zeilberger. Bifibrations of Polycategories and Classical Linear Logic. MFPS 2020 - 36th Conference on Mathematical Foundations of Programming Semantics, Jun 2020, Paris, France. pp.29-52, ⟨10.1016/j.entcs.2020.09.003⟩. ⟨hal-03031058⟩
Accès au bibtex
BibTex
ref_biblio
Davide Catta, Luc Pellissier, Christian Retoré. Inferential Semantics as Argumentative Dialogues. DCAI 2020 - 17th International Conference on Distributed Computing and Artificial Intelligence, Jun 2020, L´Aquila, Italy. pp.72-81, ⟨10.1007/978-3-030-53829-3_7⟩. ⟨hal-02922646⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02922646/file/main.pdf BibTex
ref_biblio
Matteo Cimini, Dale Miller, Jeremy G Siek. Extrinsically Typed Operational Semantics for Functional Languages. SLE 2020 - 13th ACM SIGPLAN/International Conference on Software Language Engineering, Nov 2020, Virtual, United States. ⟨hal-03007256⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03007256/file/sle2020.pdf BibTex
ref_biblio
Marianna Girlando, Bjoern Lellmann, Nicola Olivetti, Stefano Pesce, Gian Luca Pozzato. Theorem proving for Lewis Logics of Counterfactual Reasoning. CILC 2020 - 35th Edition of the Italian Conference on Computational Logic, Oct 2020, Rende / Virtual, Italy. ⟨hal-03080670⟩
Accès au texte intégral et bibtex
https://hal.science/hal-03080670/file/GirLelOliPozPesCILC2020%20camera%20ready.pdf BibTex
ref_biblio
Marianna Girlando, Lutz Strassburger. MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description). IJCAR 2020 - 10th International Joint Conference, Jul 2020, Paris, France. pp.398-407, ⟨10.1007/978-3-030-51054-1_25⟩. ⟨hal-02457240v3⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02457240/file/modal_prover.pdf BibTex
ref_biblio
Sonia Marin, Marianela Morales. Fully structured proof theory for intuitionistic modal logics. AiML 2020 - Advances in Modal Logic, Aug 2020, Helsinki, Finland. ⟨hal-03048959⟩
Accès au texte intégral et bibtex
https://hal.science/hal-03048959/file/aiml20.pdf BibTex
ref_biblio
Olivier Martinot, Gabriel Scherer. Quantified Applicatives: API design for type-inference constraints. ML Family Workshop, Aug 2020, Jersey City / Online, United States. ⟨hal-03145040⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03145040/file/quantified-applicatives-workshop-paper.pdf BibTex
ref_biblio
Francesco Mecca, Gabriel Scherer. Translation validation of a pattern-matching compiler. ML Family Workshop, Aug 2020, New Jersey /Online, United States. ⟨hal-03145030⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03145030/file/pattern-checking-workshop-paper.pdf BibTex
ref_biblio
Dale Miller. A Distributed and Trusted Web of Formal Proofs. ICDCIT 2020 - 16th International Conference on Distributed Computing and Internet Technology, Jan 2020, Bhubaneswar, India. pp.21-40, ⟨10.1007/978-3-030-36987-3_2⟩. ⟨hal-02468229⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02468229/file/icdcit-2020.pdf BibTex
ref_biblio
Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger. Deductive systems and coherence for skew prounital closed categories. LFMTP 2020 - 15th International Workshop on Logical Frameworks and Metalanguages: Theory and Practice, Jun 2020, Paris, France. pp.35-53, ⟨10.4204/eptcs.332.3⟩. ⟨hal-03031107⟩
Accès au bibtex
BibTex
ref_biblio
Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger. Eilenberg-Kelly Reloaded. MFPS 2020 - 36th Conf. on Mathematical Foundations of Programming Semantics, Jun 2020, Paris, France. pp.233-256, ⟨10.1016/j.entcs.2020.09.012⟩. ⟨hal-03031068⟩
Accès au bibtex
BibTex
ref_biblio
Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger. Proof theory of partially normal skew monoidal categories. ACT 2020 - 3rd Applied Category Theory Conference, Jul 2020, Cambridge, MA, United States. pp.230-246, ⟨10.4204/eptcs.333.16⟩. ⟨hal-03031087⟩
Accès au bibtex
BibTex

2019

ref_biblio
Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri, Claudio Sacerdoti Coen. Crumbling Abstract Machines. PPDP 2019 - 21st International Symposium on Principles and Practice of Programming Languages, Oct 2019, Porto, Portugal. ⟨10.1145/3354166.3354169⟩. ⟨hal-02415766⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02415766/file/a4-Accattoli.pdf BibTex
ref_biblio
Beniamino Accattoli. A Fresh Look at the λ-Calculus. FSCD 2019 - 4th International Conference on Formal Structures for Computation and Deduction, Jun 2019, Dortmund, Germany. ⟨10.4230/LIPIcs.FSCD.2019.1⟩. ⟨hal-02415786⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02415786/file/LIPIcs-FSCD-2019-1.pdf BibTex
ref_biblio
Beniamino Accattoli, Claudia Faggian, Giulio Guerrieri. Factorization and Normalization, Essentially. APLAS 2019 - 17th Asian Symposium on Programming Languages and Systems, Dec 2019, Bali, Indonesia. ⟨10.1007/978-3-030-34175-6_9⟩. ⟨hal-02411556⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02411556/file/1908.11289.pdf BibTex
ref_biblio
Beniamino Accattoli, Giulio Guerrieri, Maico Leberle. Types by Need. ESOP 2019 - 28th European Symposium on Programming, Apr 2019, Prague, Czech Republic. ⟨10.1007/978-3-030-17184-1_15⟩. ⟨hal-02415758⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02415758/file/Accattoli2019_Chapter_TypesByNeed.pdf BibTex
ref_biblio
Matteo Acclavio, Lutz Strassburger. On Combinatorial Proofs for Modal Logic. TABLEAUX 2019 - 28t International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Sep 2019, London, United Kingdom. pp.223-240, ⟨10.1007/978-3-030-29026-9_13⟩. ⟨hal-02390400⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02390400/file/CPKfinal.pdf BibTex
ref_biblio
Matteo Acclavio, Lutz Strassburger. On Combinatorial Proofs for Logics of Relevance and Entailment. WoLLIC 2019 - 26th International Workshop on Logic, Language, Information, and Computation, Jul 2019, Utrecht, Netherlands. pp.1-16, ⟨10.1007/978-3-662-59533-6_1⟩. ⟨hal-02390426⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02390426/file/CPrelevant.pdf BibTex
ref_biblio
Roberto Blanco, Dale Miller, Alberto Momigliano. Property-Based Testing via Proof Reconstruction. PPDP 2019 - 21st International Symposium on Principles and Practice of Programming Languages, Oct 2019, Porto, Portugal. pp.1-13, ⟨10.1145/3354166.3354170⟩. ⟨hal-02368931⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02368931/file/ppdp2019-pbt.pdf BibTex
ref_biblio
Kaustuv Chaudhuri, Matteo Manighetti, Dale Miller. A Proof-Theoretic Approach to Certifying Skolemization. CPP 2019 - 8th ACM SIGPLAN International Conference, Jan 2019, Cascais, Portugal. pp.78-90, ⟨10.1145/3293880.3294094⟩. ⟨hal-02368946⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02368946/file/skolem-draft.pdf BibTex
ref_biblio
Simon Colin, Rodolphe Lepigre, Gabriel Scherer. Unboxing Mutually Recursive Type Definitions in OCaml. JFLA 2019 - 30 èmes journées francophones des langages applicatifs, Jan 2019, Les Rousses, France. ⟨hal-01929508⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-01929508/file/1811.02300.pdf BibTex
ref_biblio
Andrea Condoluci, Beniamino Accattoli, Claudio Sacerdoti Coen. Sharing Equality is Linear. PPDP 2019 - 21st International Symposium on Principles and Practice of Programming Languages, Oct 2019, Porto, Portugal. ⟨10.1145/3354166.3354174⟩. ⟨hal-02415769⟩
Accès au texte intégral et bibtex
https://hal.science/hal-02415769/file/a9-Condoluci.pdf BibTex
ref_biblio
Ulysse Gérard, Dale Miller, Gabriel Scherer. Functional programming with $λ$-tree syntax. PPDP 2019 - 21st International Symposium on Principles and Practice of Programming Languages, Oct 2019, Porto, Portugal. pp.1-16, ⟨10.1145/3354166.3354177⟩. ⟨hal-02368906⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02368906/file/mlts-2019.pdf BibTex
ref_biblio
Willem Heijltjes, Dominic J D Hughes, Lutz Strassburger. Intuitionistic proofs without syntax. LICS 2019 - 34th Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2019, Vancouver, Canada. pp.1-13, ⟨10.1109/LICS.2019.8785827⟩. ⟨hal-02386878⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02386878/file/icp.pdf BibTex
ref_biblio
Willem Heijltjes, Dominic J D Hughes, Lutz Strassburger. Proof Nets for First-Order Additive Linear Logic. FSCD 2019 - 4th International Conference on Formal Structures for Computation and Deduction, Jun 2019, Dortmund, Germany. pp.22:1-22:22, ⟨10.4230/LIPIcs.FSCD.2019.22⟩. ⟨hal-02386942⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02386942/file/LIPIcs-FSCD-2019-22.pdf BibTex
ref_biblio
Benjamin Ralph, Lutz Strassburger. Towards a Combinatorial Proof Theory. TABLEAUX 2019 - 28th International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, Sep 2019, London, United Kingdom. pp.259-276, ⟨10.1007/978-3-030-29026-9_15⟩. ⟨hal-02390417⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02390417/file/CPT.pdf BibTex

2018

ref_biblio
Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger. The Sequent Calculus of Skew Monoidal Categories. Proc. of 34th Conf. on Mathematical Foundations of Programming Semantics, MFPS XXXIV, Jun 2018, Halifax, Canada. pp.345-370, ⟨10.1016/j.entcs.2018.11.017⟩. ⟨hal-03031126⟩
Accès au bibtex
https://arxiv.org/pdf/2003.05213 BibTex
ref_biblio
Noam Zeilberger. A theory of linear typings as flows on 3-valent graphs. LICS '18: 33rd Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2018, Oxford United Kingdom, France. pp.919-928, ⟨10.1145/3209108.3209121⟩. ⟨hal-03132231⟩
Accès au bibtex
https://arxiv.org/pdf/1804.10540 BibTex

Book sections

2024

ref_biblio
Farah Al Wardani, Kaustuv Chaudhuri, Dale Miller. About Trust and Proof: An experimental framework for heterogeneous verification. The Practice of Formal Methods, LNCS 14781, Springer Nature Switzerland, pp.162-183, 2024, Essays in Honour of Cliff Jones, Part II, 978-3-031-66672-8. ⟨10.1007/978-3-031-66673-5_9⟩. ⟨hal-04710949⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04710949/file/damf-About-Trust-and-Proof-2024.pdf BibTex

2020

ref_biblio
Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger. The sequent calculus of skew monoidal categories (extended version). C. Casadio; P. J. Scott. Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics, Springer, In press, Outstanding Contributions to Logic. ⟨hal-03031139⟩
Accès au bibtex
BibTex

Lectures

2021

ref_biblio
Willem Heijltjes, Lutz Strassburger. From Proof Nets to Combinatorial Proofs - A New Approach to Hilbert's 24th Problem. École thématique. From Proof Nets to Combinatorial Proofs - A New Approach to Hilbert's 24th Problem, Utrecht / Virtual, Netherlands. 2021. ⟨hal-03316571⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03316571/file/full.pdf BibTex

2019

ref_biblio
Andrea Aler Tubella, Lutz Strassburger. Introduction to Deep Inference. École thématique. Introduction to Deep Inference, Riga, Latvia. 2019. ⟨hal-02390267⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02390267/file/ESSLLI19notes.pdf BibTex

Books

2012

ref_biblio
Gramlich Bernhard, Dale Miller, Sattler Uli. Automated Reasoning: 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 2012, Proceedings. Springer, 7364, pp.1-568, 2012, Lecture Notes in Artificial Intelligence, ⟨10.1007/978-3-642-31365-3⟩. ⟨hal-00776254⟩
Accès au bibtex
BibTex

Reports

2020

ref_biblio
Roberto Blanco, Matteo Manighetti, Dale Miller. FPC-Coq: Using ELPI to elaborate external proof evidence into Coq proofs. [Research Report] Inria Saclay. 2020. ⟨hal-02974002⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-02974002/file/fpccoq-draft.pdf BibTex

Theses

2023

ref_biblio
Matteo Manighetti. Developing proof theory for proof exchange. Logic in Computer Science [cs.LO]. Institut Polytechnique de Paris, 2023. English. ⟨NNT : 2023IPPAX003⟩. ⟨tel-04289251⟩
Accès au texte intégral et bibtex
https://theses.hal.science/tel-04289251/file/94295_MANIGHETTI_2023_archivage.pdf BibTex

Preprints, Working Papers, ...

2024

ref_biblio
Beniamino Accattoli, Adrienne Lancelot. Light Genericity. 2024. ⟨hal-04406343⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04406343/file/main.pdf BibTex
ref_biblio
Beniamino Accattoli, Jui-Hsuan Wu. Positive Focusing is Directly Useful. 2024. ⟨hal-04606194⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04606194/file/main.pdf BibTex
ref_biblio
Matteo Manighetti, Dale Miller. Peano Arithmetic and μMALL. 2024. ⟨hal-04824175⟩
Accès au texte intégral et bibtex
https://hal.science/hal-04824175/file/2312.13634v2.pdf BibTex

2023

ref_biblio
Farah Al Wardani, Kaustuv Chaudhuri, Dale Miller. Distributing and trusting proof checking: a preliminary report. 2023. ⟨hal-03909741v2⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03909741/file/paper.pdf BibTex

2022

ref_biblio
Kaustuv Chaudhuri, Pablo Donato, Luigi Massacci, Benjamin Werner. Certifying Proof-By-Linking. 2022. ⟨hal-04317972⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04317972/file/main.pdf BibTex
ref_biblio
Bryce Clarke, Matthew Di Meglio. An introduction to enriched cofunctors. 2022. ⟨hal-03805364⟩
Accès au texte intégral et bibtex
https://hal.science/hal-03805364/file/arXiv-version.pdf BibTex
ref_biblio
Matteo Manighetti, Dale Miller. Computational logic based on linear logic and fixed points. 2022. ⟨hal-03579451⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-03579451/file/root.pdf BibTex

2021

ref_biblio
Matteo Acclavio, Davide Catta, Lutz Strassburger. Towards a Denotational Semantics for Proofs in Constructive Modal Logic. 2021. ⟨hal-03201439⟩
Accès au texte intégral et bibtex
https://hal.science/hal-03201439/file/ICP%2BWIS.pdf BibTex
ref_biblio
Olivier Bodini, Alexandros Singh, Noam Zeilberger. Asymptotic Distribution of Parameters in Trivalent Maps and Linear Lambda Terms. 2021. ⟨hal-03495894⟩
Accès au bibtex
https://arxiv.org/pdf/2106.08291 BibTex
ref_biblio
Chuck Liang, Dale Miller. Focusing Gentzen's LK proof system. 2021. ⟨hal-03457379⟩
Accès au texte intégral et bibtex
https://hal.science/hal-03457379/file/lkf-2021-03-31.pdf BibTex

2020

ref_biblio
Marianna Girlando, Marianela Morales. MOILab: towards a labelled theorem prover for intuitionistic modal logics. 2020. ⟨hal-03048966⟩
Accès au texte intégral et bibtex
https://hal.science/hal-03048966/file/WiL_moiLab.pdf BibTex

2005

ref_biblio
Gilles Dowek, Benjamin Werner. A constructive proof of Skolem theorem for constructive logic. 2005. ⟨hal-04099179⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04099179/file/skolem.pdf BibTex
?
?
?
?
?
?
?
?

Institut Polytechnique de Paris

5, Avenue Le Chatelier
F-91764 Palaiseau Cedex France

Ⓒ 2020–2025 Institut Polytechnique de Paris