CSDAI

Journal articles

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2024

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

2019

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

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

Preprints, Working Papers, ...

2024

ref_biblio

Beniamino Accattoli, Adrienne Lancelot. Light Genericity. 2024. ⟨hal-04406343⟩

Accès au texte intégral et bibtex

ref_biblio

Beniamino Accattoli, Jui-Hsuan Wu. Positive Focusing is Directly Useful. 2024. ⟨hal-04606194⟩

Accès au texte intégral et bibtex

ref_biblio

Bryce Clarke. Lifting twisted coreflections against delta lenses. 2024. ⟨hal-04430822⟩

Accès au texte intégral et bibtex

ref_biblio

Matteo Manighetti, Dale Miller. Peano Arithmetic and μMALL. 2024. ⟨hal-04824175⟩

Accès au texte intégral et 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

ref_biblio

Paul-André Melliès, Noam Zeilberger. The categorical contours of the Chomsky-Schützenberger representation theorem. 2023. ⟨hal-04399404⟩

Accès au texte intégral et 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

ref_biblio

Bryce Clarke, Matthew Di Meglio. An introduction to enriched cofunctors. 2022. ⟨hal-03805364⟩

Accès au texte intégral et 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

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

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

ref_biblio

Chuck Liang, Dale Miller. Focusing Gentzen's LK proof system. 2021. ⟨hal-03457379⟩

Accès au texte intégral et 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

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