CSDAI Department

Journal articles

2021

ref_biblio

Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni. The (In)Efficiency of interaction. Proceedings of the ACM on Programming Languages, ACM, 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, Oxford University Press (OUP), 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, Springer Verlag, 2021, ⟨10.1007/s10472-021-09774-y⟩. ⟨hal-03457303⟩

Accès au bibtex

ref_biblio

Sonia Marin, Marianela Morales, Lutz Straßburger. A fully labelled proof system for intuitionistic modal logics. Journal of Logic and Computation, Oxford University Press (OUP), 2021, 31 (3), pp.998-1022. ⟨10.1093/logcom/exab020⟩. ⟨hal-02390454v3⟩

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, Springer Verlag, 2021, ⟨10.1007/s10472-021-09764-0⟩. ⟨hal-03457312⟩

Accès au bibtex

ref_biblio

Dale Miller. Reciprocal Influences Between Proof Theory and Logic Programming. Philosophy & Technology, Springer, 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. A Survey of the Proof-Theoretic Foundations of Logic Programming. Theory and Practice of Logic Programming, Cambridge University Press (CUP), 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, ACM, 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, Cambridge University Press (CUP), 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, Logical Methods in Computer Science Association, 2019, 15 (1), pp.1-23. ⟨10.23638/LMCS-15(1:9)2019⟩. ⟨hal-03131847⟩

Accès au bibtex

Conference papers

2022

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

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

Accès au texte intégral et bibtex

ref_biblio

Willem Heijltjes, Dominic Hughes, Lutz Straßburger. Normalization Without Syntax. FSCD 2022, Aug 2022, Haifa, Israel. ⟨hal-03654060⟩

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

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

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 Straßburger. 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 Straßburger, Dominic 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, 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

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

Matteo Acclavio, Ross Horne, Lutz Straßburger. 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 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 Straßburger. 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. 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

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

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

2021

ref_biblio

Matteo Acclavio, Davide Catta, Lutz Straßburger. Game Semantics for Constructive Modal Logic. Automated Reasoning with Analytic Tableaux and Related Methods, 12842, Springer International Publishing, pp.428-445, 2021, Lecture Notes in Computer Science, ⟨10.1007/978-3-030-86059-2_25⟩. ⟨hal-03369819⟩

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 Straßburger. 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

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

2022

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 Straßburger. 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

Matteo Acclavio, Ross Horne, Lutz Straßburger. An Analytic Propositional Proof System On Graphs. 2020. ⟨hal-03087392⟩

Accès au texte intégral et bibtex

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