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

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: Stacked Implementations in Camlboot. 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

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
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
https://arxiv.org/pdf/2109.01483 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
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

2023

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
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-04169014⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04169014/file/HAL-subm.zip 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

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. ⟨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, 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, 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, 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
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
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
https://inria.hal.science/hal-03369764/file/2104.13124.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, 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
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
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

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

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

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
https://hal.science/hal-03912170/file/template.pdf 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
https://inria.hal.science/hal-02974002/file/fpccoq-draft.pdf 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
https://inria.hal.science/hal-03909741/file/paper.pdf BibTex
ref_biblio
Bryce Clarke. The Algebraic Weak Factorisation System for Delta Lenses. 2023. ⟨hal-04089742⟩
Accès au texte intégral et bibtex
https://inria.hal.science/hal-04089742/file/Clarke-ACT2023-submitted.pdf 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
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
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
https://inria.hal.science/hal-03909547/file/2209.07825.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–2023 Institut Polytechnique de Paris