CSDAI

Journal articles

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

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

Dale Miller. A Survey of the Proof-Theoretic Foundations of Logic Programming. Theory and Practice of Logic Programming, 2021, pp.1-46. ⟨10.1017/S1471068421000533⟩. ⟨hal-03411144⟩

Accès au 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

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

2023

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

2022

ref_biblio

Beniamino Accattoli. Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic. LICS '22: 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Aug 2022, Haifa Israel, France. 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. 7th International Conference on Formal Structures for Computation and Deduction (FSCD 2022), 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. Advances in Modal Logic 2022, 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. Advances in Modal Logic 2022, 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. ⟨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. 30th EACSL Annual Conference on Computer Science Logic, CSL 2022, 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. Logic, Language, Information, and Computation - 28th International Workshop, WoLLIC 2022, 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

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

ref_biblio

Lutz Strassburger, Dominic J D Hughes, 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

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, 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

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

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. 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. 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. 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

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

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

Reports

2022

ref_biblio

Wendlasida Ouedraogo, Lutz Strassburger, Gabriel Scherer. Coqlex: Generating Formally Verified Lexers. INRIA Saclay - Ile-de-France. 2022. ⟨hal-03912170⟩

Accès au texte intégral et bibtex

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

Preprints, Working Papers, ...

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

Bryce Clarke. The Algebraic Weak Factorisation System for Delta Lenses. 2023. ⟨hal-04089742⟩

Accès au texte intégral et bibtex

2022

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

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. 2022. ⟨hal-03909547⟩

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