2024
Conference papers
- titre
- Correct tout seul, sûr à plusieurs
- auteur
- Clément Allain, Gabriel Scherer
- article
- JFLA 2024 – 35es Journ´ees Francophones des Langages Applicatifs, Jan 2024, Saint-Jacut-de-la-Mer, France
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, …
- titre
- The Flower Calculus
- auteur
- Pablo Donato
- article
- 2024
- Accès au texte intégral et bibtex
-
- titre
- Lifting twisted coreflections against delta lenses
- auteur
- Bryce Clarke
- article
- 2024
- Accès au texte intégral et bibtex
-
- titre
- Light Genericity
- auteur
- Beniamino Accattoli, Adrienne Lancelot
- article
- 2024
- Accès au texte intégral et bibtex
-
2023
Journal articles
- titre
- A System of Interaction and Structure III: The Complexity of BV and Pomset Logic
- auteur
- Lê Thành Dũng Nguyên, Lutz Straßburger
- article
- Logical Methods in Computer Science, 2023, 9 (4), ⟨10.46298/LMCS-19(4:25)2023⟩
- Accès au texte intégral et bibtex
-
- titre
- Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
- auteur
- Beniamino Accattoli
- article
- Logical Methods in Computer Science, 2023, Volume 19, Issue 4, ⟨10.46298/lmcs-19(4:23)2023⟩
- Accès au bibtex
-
- titre
- Coqlex: Generating Formally Verified Lexers
- auteur
- Wendlasida Ouedraogo, Lutz Strassburger, Gabriel Scherer
- article
- The Art, Science, and Engineering of Programming, 2023, 8 (1), ⟨10.22152/programming-journal.org/2024/8/3⟩
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Strong Call-by-Value and Multi Types
- auteur
- Beniamino Accattoli, Giulio Guerrieri, Maico Leberle
- article
- ICTAC 2023 – 20th International Colloquium on Theoretical Aspects of Computing, Dec 2023, Lima, Peru
- Accès au texte intégral et bibtex
-
- titre
- Proofs as Terms, Terms as Graphs
- auteur
- Jui-Hsuan Wu
- article
- APLAS 2023 – 21st Asian Symposium on Programming Languages and Systems, Nov 2023, Taipei, Taiwan
- Accès au texte intégral et bibtex
-
- titre
- A Diamond Machine for Strong Evaluation
- auteur
- Beniamino Accattoli, Pablo Barenbaum
- article
- APLAS 2023 – The 21st Asian Symposium on Programming Languages and Systems, Nov 2023, Taipei, Taiwan
- Accès au texte intégral et bibtex
-
- titre
- Sharing a Perspective on the lambda Calculus
- auteur
- Beniamino Accattoli
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- Formal Reasoning using Distributed Assertions
- auteur
- Farah Al Wardani, Kaustuv Chaudhuri, Dale Miller
- article
- FroCoS 2023 – 14th International Symposium on Frontiers of Combining Systems, Sep 2023, Prague (Czech Republic), Czech Republic
- Accès au texte intégral et bibtex
-
- titre
- The Algebraic Weak Factorisation System for Delta Lenses
- auteur
- Bryce Clarke
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- Formalizing Functions as Processes
- auteur
- Beniamino Accattoli, Horace Blanc, Claudio Sacerdoti Coen
- article
- ITP 2023 – 14th International Conference on Interactive Theorem Proving, Jul 2023, Bialystok, Poland. ⟨10.4230/LIPICS.ITP.2023.5⟩
- Accès au texte intégral et bibtex
-
- titre
- Convolution Products on Double Categories and Categorification of Rule Algebras
- auteur
- Nicolas Behr, Paul-André Melliès, Noam Zeilberger
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- Intuitionistic S4 is decidable
- auteur
- Marianna Girlando, Roman Kuznets, Sonia Marin, Marianela Morales, Lutz Strassburger
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- A system of inference based on proof search: an extended abstract
- auteur
- Dale Miller
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- A positive perspective on term representation: Extended paper
- auteur
- Dale Miller, Jui-Hsuan Wu
- article
- CSL 2023 – Computer Science Logic, Feb 2023, Warsaw, Poland
- Accès au texte intégral et bibtex
-
- titre
- Backtracking reference stores
- auteur
- Camille Noûs, Gabriel Scherer
- article
- JFLA 2023 – 34èmes Journées Francophones des Langages Applicatifs, Jan 2023, Praz-sur-Arly, France. pp.190-210
- Accès au texte intégral et bibtex
-
Theses
- titre
- Developing proof theory for proof exchange
- auteur
- Matteo Manighetti
- article
- Logic in Computer Science [cs.LO]. Institut Polytechnique de Paris, 2023. English. ⟨NNT : 2023IPPAX003⟩
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, …
- titre
- The categorical contours of the Chomsky-Schützenberger representation theorem
- auteur
- Paul-André Melliès, Noam Zeilberger
- article
- 2023
- Accès au texte intégral et bibtex
-
- titre
- Distributing and trusting proof checking: a preliminary report
- auteur
- Farah Al Wardani, Kaustuv Chaudhuri, Dale Miller
- article
- 2023
- Accès au texte intégral et bibtex
-
2022
Journal articles
- titre
- An Analytic Propositional Proof System On Graphs
- auteur
- Matteo Acclavio, Ross Horne, Lutz Strassburger
- article
- Logical Methods in Computer Science, 2022, 18 (4), ⟨10.46298/LMCS-18(4:1)2022⟩
- Accès au texte intégral et bibtex
-
- titre
- The theory of call-by-value solvability
- auteur
- Beniamino Accattoli, Giulio Guerrieri
- article
- Proceedings of the ACM on Programming Languages, 2022, 6 (ICFP), pp.855-885. ⟨10.1145/3547652⟩
- Accès au bibtex
-
- titre
- Multi Types and Reasonable Space
- auteur
- Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
- article
- Proceedings of the ACM on Programming Languages, 2022, 6 (ICFP), pp.799-825. ⟨10.1145/3547650⟩
- Accès au bibtex
-
- titre
- From axioms to synthetic inference rules via focusing
- auteur
- Sonia Marin, Dale Miller, Elaine Pimentel, Marco Volpe
- article
- Annals of Pure and Applied Logic, 2022, 173 (5), pp.103091. ⟨10.1016/j.apal.2022.103091⟩
- Accès au texte intégral et bibtex
-
- titre
- Debootstrapping without Archeology
- auteur
- Nathanaëlle Courant, Julien Lepiller, Gabriel Scherer
- article
- The Art, Science, and Engineering of Programming, 2022, 6 (3), ⟨10.22152/programming-journal.org/2022/6/13⟩
- Accès au texte intégral et bibtex
-
- titre
- A Survey of the Proof-Theoretic Foundations of Logic Programming
- auteur
- Dale Miller
- article
- Theory and Practice of Logic Programming, 2022, 22 (6), pp.859 – 904. ⟨10.1017/S1471068421000533⟩
- Accès au bibtex
-
Conference papers
- titre
- Combinatorial Flows as Bicolored Atomic Flows
- auteur
- Giti Omidvar, Lutz Straßburger
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- An OCaml use case for strong call-by-need reduction
- auteur
- Gabriel Scherer, Nathanaëlle Courant
- article
- ACM SIGPLAN Workshop on ML 2022 – ML Family Workshop, Benoit Montagu, Sep 2022, Ljubljana, Slovenia
- Accès au texte intégral et bibtex
-
- titre
- Boxroot, fast movable GC roots for a better FFI
- auteur
- Guillaume Munch-Maccagnoni, Gabriel Scherer
- article
- ML Family Workshop, Benoît Montagu, Sep 2022, Ljubljana, Slovenia
- Accès au texte intégral et bibtex
-
- titre
- Taming Bounded Depth with Nested Sequents
- auteur
- Agata Ciabattoni, Lutz Straßburger, Matteo Tesi
- article
- AIML 2022 – Advances in Modal Logic, Aug 2022, Rennes, France
- Accès au texte intégral et bibtex
-
- titre
- Combinatorial Proofs for Constructive Modal Logic
- auteur
- Matteo Acclavio, Lutz Straßburger
- article
- AiML 2022 – Advances in Modal Logic, Aug 2022, Rennes, France
- Accès au texte intégral et bibtex
-
- titre
- Normalization Without Syntax
- auteur
- Willem Heijltjes, Dominic Hughes, Lutz Strassburger
- article
- FSCD 2022, Aug 2022, Haifa, Israel
- Accès au texte intégral et bibtex
-
- titre
- Exponentials as Substitutions and the Cost of Cut Elimination in Linear Logic
- auteur
- Beniamino Accattoli
- article
- LICS 2022 – 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Aug 2022, Haifa, Israel. pp.1-15, ⟨10.1145/3531130.3532445⟩
- Accès au bibtex
-
- titre
- Reasonable Space for the λ-Calculus, Logarithmically
- auteur
- Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
- article
- LICS 2022 – 37th Annual ACM/IEEE Symposium on Logic in Computer Science, Aug 2022, Haifa, Israel. pp.1-13, ⟨10.1145/3531130.3533362⟩
- Accès au bibtex
-
- titre
- A Graphical Proof Theory of Logical Time
- auteur
- Matteo Acclavio, Ross Horne, Sjouke Mauw, Lutz Straßburger
- article
- FSCD 2022 – 7th International Conference on Formal Structures for Computation and Deduction, Aug 2022, Haifa, Israel. ⟨10.4230/LIPIcs.FSCD.2022.22⟩
- Accès au texte intégral et bibtex
-
- titre
- Parsing as a lifting problem and the Chomsky-Schützenberger representation theorem
- auteur
- Paul-André Melliès, Noam Zeilberger
- article
- MFPS 2022 – 38th conference on Mathematical Foundations for Programming Semantics, Jul 2022, Ithaca, NY, United States. ⟨10.46298/entics.10508⟩
- Accès au texte intégral et bibtex
-
- titre
- Actema : une interface graphique et gestuelle pour preuves formelles (démonstration)
- auteur
- Pablo Donato, Pierre-Yves Strub, Benjamin Werner
- article
- 33èmes Journées Francophones des Langages Applicatifs, Jun 2022, Saint-Médard-d’Excideuil, France. pp.267-268
- Accès au texte intégral et bibtex
-
- titre
- BV and Pomset Logic Are Not the Same
- auteur
- Lê Thành Dung Nguyên, Lutz Straßburger
- article
- CSL 2022 – 30th EACSL Annual Conference on Computer Science Logic, Feb 2022, Göttingen, Germany. ⟨10.4230/LIPIcs.CSL.2022.32⟩
- Accès au texte intégral et bibtex
-
- titre
- Useful Open Call-By-Need
- auteur
- Beniamino Accattoli, Maico Leberle
- article
- CSL 2022 – 30th EACSL Annual Conference on Computer Science Logic, Feb 2022, Gottingen, Germany. ⟨10.4230/LIPIcs.CSL.2022.4⟩
- Accès au texte intégral et bibtex
-
- titre
- Déboîter les constructeurs
- auteur
- Nicolas Chataing, Camille Noûs, Gabriel Scherer
- article
- Journées Francophones des Langages Applicatifs, Feb 2022, Saint-Médard-d’Excideuil, France
- Accès au texte intégral et bibtex
-
- titre
- A drag-and-drop proof tactic
- auteur
- Pablo Donato, Pierre-Yves Strub, Benjamin Werner
- article
- CPP 2022: 11th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2022, Philadelphia, United States. pp.197-209, ⟨10.1145/3497775.3503692⟩
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, …
- titre
- Certifying Proof-By-Linking
- auteur
- Kaustuv Chaudhuri, Pablo Donato, Luigi Massacci, Benjamin Werner
- article
- 2022
- Accès au texte intégral et bibtex
-
- titre
- An introduction to enriched cofunctors
- auteur
- Bryce Clarke, Matthew Di Meglio
- article
- 2022
- Accès au texte intégral et bibtex
-
- titre
- Computational logic based on linear logic and fixed points
- auteur
- Matteo Manighetti, Dale Miller
- article
- 2022
- Accès au texte intégral et bibtex
-
2021
Journal articles
- titre
- Functions-as-constructors higher-order unification: extended pattern unification
- auteur
- Tomer Libal, Dale Miller
- article
- Annals of Mathematics and Artificial Intelligence, 2021, ⟨10.1007/s10472-021-09774-y⟩
- Accès au bibtex
-
- titre
- The undecidability of proof search when equality is a logical connective
- auteur
- Dale Miller, Alexandre Viel
- article
- Annals of Mathematics and Artificial Intelligence, 2021, ⟨10.1007/s10472-021-09764-0⟩
- Accès au texte intégral et bibtex
-
- titre
- A fully labelled proof system for intuitionistic modal logics
- auteur
- Sonia Marin, Marianela Morales, Lutz Strassburger
- article
- Journal of Logic and Computation, 2021, 31 (3), pp.998-1022. ⟨10.1093/logcom/exab020⟩
- Accès au texte intégral et bibtex
-
- titre
- A practical mode system for recursive definitions
- auteur
- Alban Reynaud, Gabriel Scherer, Jeremy Yallop
- article
- Proceedings of the ACM on Programming Languages, 2021, 5 (POPL), pp.1-29. ⟨10.1145/3434326⟩
- Accès au texte intégral et bibtex
-
- titre
- The (In)Efficiency of interaction
- auteur
- Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
- article
- Proceedings of the ACM on Programming Languages, 2021, 5 (POPL), pp.1-33. ⟨10.1145/3434332⟩
- Accès au texte intégral et bibtex
-
- titre
- Reciprocal Influences Between Proof Theory and Logic Programming
- auteur
- Dale Miller
- article
- Philosophy & Technology, 2021, 34, pp.75-104. ⟨10.1007/s13347-019-00370-x⟩
- Accès au texte intégral et bibtex
-
- titre
- Uniform labelled calculi for preferential conditional logics based on neighbourhood semantics
- auteur
- Marianna Girlando, Sara Negri, Nicola Olivetti
- article
- Journal of Logic and Computation, 2021, 31 (3), pp.947-997. ⟨10.1093/logcom/exab019⟩
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Game Semantics for Constructive Modal Logic
- auteur
- Matteo Acclavio, Davide Catta, Lutz Strassburger
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- Unfolding ML datatype declarations without loops
- auteur
- Nicolas Chataing, Gabriel Scherer
- article
- ML Family Workshop, Aug 2021, online, South Korea
- Accès au texte intégral et bibtex
-
- titre
- Frozen inference constraints for type-directed disambiguation
- auteur
- Olivier Martinot, Gabriel Scherer
- article
- ML Family Workshop, Aug 2021, online, South Korea
- Accès au texte intégral et bibtex
-
- titre
- Demo Paper: Coqlex, an approach to generate verified lexers
- auteur
- Wendlasida Ouedraogo, Danko Ilik, Lutz Strassburger
- article
- ML 2021-ACM SIGPLAN Workshop on ML, Aug 2021, Online event, United States
- Accès au texte intégral et bibtex
-
- titre
- Subformula Linking for Intuitionistic Logic with Application to Type Theory
- auteur
- Kaustuv Chaudhuri
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- The Space of Interaction
- auteur
- Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
- article
- LICS 2021 – 36th Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2021, Rome, France. pp.1-13, ⟨10.1109/LICS52264.2021.9470726⟩
- Accès au texte intégral et bibtex
-
- titre
- Strong Call-by-Value is Reasonable, Implosively
- auteur
- Beniamino Accattoli, Andrea Condoluci, Claudio Sacerdoti Coen
- article
- 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jun 2021, Rome, Italy. pp.1-14, ⟨10.1109/LICS52264.2021.9470630⟩
- Accès au bibtex
-
- titre
- Combinatorial Proofs and Decomposition Theorems for First-order Logic
- auteur
- Dominic J D Hughes, Lutz Strassburger, Jui-Hsuan Wu
- article
- 2021 36th Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jun 2021, Rome, Italy. pp.1-13, ⟨10.1109/LICS52264.2021.9470579⟩
- Accès au texte intégral et bibtex
-
- titre
- Tail Modulo Cons
- auteur
- Frédéric Bour, Basile Clément, Gabriel Scherer
- article
- JFLA 2021 – Journées Francophones des Langages Applicatifs, Apr 2021, Saint Médard d’Excideuil, France
- Accès au texte intégral et bibtex
-
- titre
- Factorize Factorization
- auteur
- Beniamino Accattoli, Claudia Faggian, Giulio Guerrieri
- article
- CSL 2021 – 29th EACSL Annual Conference on Computer Science Logic, Jan 2021, Ljubljana, Slovenia. ⟨10.4230/LIPIcs.CSL.2021.22⟩
- Accès au texte intégral et bibtex
-
Lectures
- titre
- From Proof Nets to Combinatorial Proofs – A New Approach to Hilbert’s 24th Problem
- auteur
- Willem Heijltjes, Lutz Strassburger
- article
- École thématique. From Proof Nets to Combinatorial Proofs – A New Approach to Hilbert’s 24th Problem, Utrecht / Virtual, Netherlands. 2021
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, …
- titre
- Asymptotic Distribution of Parameters in Trivalent Maps and Linear Lambda Terms
- auteur
- Olivier Bodini, Alexandros Singh, Noam Zeilberger
- article
- 2021
- Accès au bibtex
-
- titre
- Focusing Gentzen’s LK proof system
- auteur
- Chuck Liang, Dale Miller
- article
- 2021
- Accès au texte intégral et bibtex
-
- titre
- Towards a Denotational Semantics for Proofs in Constructive Modal Logic
- auteur
- Matteo Acclavio, Davide Catta, Lutz Strassburger
- article
- 2021
- Accès au texte intégral et bibtex
-
2020
Journal articles
- titre
- Tight typings and split bounds, fully developed
- auteur
- Beniamino Accattoli, Stéphane Graham-Lengrand, Delia Kesner
- article
- Journal of Functional Programming, 2020, 30, ⟨10.1017/S095679682000012X⟩
- Accès au bibtex
-
Conference papers
- titre
- Extrinsically Typed Operational Semantics for Functional Languages
- auteur
- Matteo Cimini, Dale Miller, Jeremy G Siek
- article
- SLE 2020 – 13th ACM SIGPLAN/International Conference on Software Language Engineering, Nov 2020, Virtual, United States
- Accès au texte intégral et bibtex
-
- titre
- Theorem proving for Lewis Logics of Counterfactual Reasoning
- auteur
- Marianna Girlando, Bjoern Lellmann, Nicola Olivetti, Stefano Pesce, Gian Luca Pozzato
- article
- CILC 2020 – 35th Edition of the Italian Conference on Computational Logic, Oct 2020, Rende / Virtual, Italy
- Accès au texte intégral et bibtex
-
- titre
- Functional Pearl: The Distributive $\lambda$-Calculus
- auteur
- Beniamino Accattoli, Alejandro Díaz-Caro
- article
- 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⟩
- Accès au bibtex
-
- titre
- The Machinery of Interaction
- auteur
- Beniamino Accattoli, Ugo Dal Lago, Gabriele Vanoni
- article
- PPDP ’20 – 22nd International Symposium on Principles and Practice of Declarative Programming, Sep 2020, Bologna, Italy. pp.1-15, ⟨10.1145/3414080.3414108⟩
- Accès au bibtex
-
- titre
- Quantified Applicatives: API design for type-inference constraints
- auteur
- Olivier Martinot, Gabriel Scherer
- article
- ML Family Workshop, Aug 2020, Jersey City / Online, United States
- Accès au texte intégral et bibtex
-
- titre
- Translation validation of a pattern-matching compiler
- auteur
- Francesco Mecca, Gabriel Scherer
- article
- ML Family Workshop, Aug 2020, New Jersey /Online, United States
- Accès au texte intégral et bibtex
-
- titre
- Fully structured proof theory for intuitionistic modal logics
- auteur
- Sonia Marin, Marianela Morales
- article
- AiML 2020 – Advances in Modal Logic, Aug 2020, Helsinki, Finland
- Accès au texte intégral et bibtex
-
- titre
- Logic beyond formulas: a proof system on graphs
- auteur
- Matteo Acclavio, Ross Horne, Lutz Strassburger
- article
- LICS 2020 – 35th ACM/IEEE Symposium on Logic in Computer Science, Jul 2020, Saarbrücken, Germany. pp.38-52, ⟨10.1145/3373718.3394763⟩
- Accès au texte intégral et bibtex
-
- titre
- Proof theory of partially normal skew monoidal categories
- auteur
- Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger
- article
- ACT 2020 – 3rd Applied Category Theory Conference, Jul 2020, Cambridge, MA, United States. pp.230-246, ⟨10.4204/eptcs.333.16⟩
- Accès au bibtex
-
- titre
- MOIN: A Nested Sequent Theorem Prover for Intuitionistic Modal Logics (System Description)
- auteur
- Marianna Girlando, Lutz Strassburger
- article
- IJCAR 2020 – 10th International Joint Conference, Jul 2020, Paris, France. pp.398-407, ⟨10.1007/978-3-030-51054-1_25⟩
- Accès au texte intégral et bibtex
-
- titre
- Deductive systems and coherence for skew prounital closed categories
- auteur
- Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger
- article
- 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⟩
- Accès au bibtex
-
- titre
- Inferential Semantics as Argumentative Dialogues
- auteur
- Davide Catta, Luc Pellissier, Christian Retoré
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- Eilenberg-Kelly Reloaded
- auteur
- Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger
- article
- MFPS 2020 – 36th Conf. on Mathematical Foundations of Programming Semantics, Jun 2020, Paris, France. pp.233-256, ⟨10.1016/j.entcs.2020.09.012⟩
- Accès au bibtex
-
- titre
- Bifibrations of Polycategories and Classical Linear Logic
- auteur
- Nicolas Blanco, Noam Zeilberger
- article
- MFPS 2020 – 36th Conference on Mathematical Foundations of Programming Semantics, Jun 2020, Paris, France. pp.29-52, ⟨10.1016/j.entcs.2020.09.003⟩
- Accès au bibtex
-
- titre
- Generalized connectives for multiplicative linear logic
- auteur
- Matteo Acclavio, Roberto Maieli
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- A Distributed and Trusted Web of Formal Proofs
- auteur
- Dale Miller
- article
- 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⟩
- Accès au texte intégral et bibtex
-
Book sections
- titre
- The sequent calculus of skew monoidal categories (extended version)
- auteur
- Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger
- article
- C. Casadio; P. J. Scott. Joachim Lambek: The Interplay of Mathematics, Logic, and Linguistics, Springer, In press, Outstanding Contributions to Logic
- Accès au bibtex
-
Reports
- titre
- FPC-Coq: Using ELPI to elaborate external proof evidence into Coq proofs
- auteur
- Roberto Blanco, Matteo Manighetti, Dale Miller
- article
- [Research Report] Inria Saclay. 2020
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, …
- titre
- MOILab: towards a labelled theorem prover for intuitionistic modal logics
- auteur
- Marianna Girlando, Marianela Morales
- article
- 2020
- Accès au texte intégral et bibtex
-
2019
Journal articles
- titre
- A proof theory for model checking
- auteur
- Quentin Heath, Dale Miller
- article
- Journal of Automated Reasoning, 2019, 63 (4), pp.857-885. ⟨10.1007/s10817-018-9475-3⟩
- Accès au texte intégral et bibtex
-
- titre
- Connected chord diagrams and bridgeless maps
- auteur
- Julien Courtiel, Karen Yeats, Noam Zeilberger
- article
- The Electronic Journal of Combinatorics, 2019, 26 (4), pp.1-56. ⟨10.37236/7400⟩
- Accès au texte intégral et bibtex
-
- titre
- Mechanized metatheory revisited
- auteur
- Dale Miller
- article
- Journal of Automated Reasoning, 2019, 63 (3), pp.625-665. ⟨10.1007/s10817-018-9483-3⟩
- Accès au texte intégral et bibtex
-
- titre
- Deep inference and expansion trees for second-order multiplicative linear logic
- auteur
- Lutz Strassburger
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- Formalized meta-theory of sequent calculi for linear logics
- auteur
- Kaustuv Chaudhuri, Leonardo Lima, Giselle Reis
- article
- Theoretical Computer Science, 2019, 781, pp.24-38. ⟨10.1016/j.tcs.2019.02.023⟩
- Accès au texte intégral et bibtex
-
- titre
- On the decision problem for MELL
- auteur
- Lutz Strassburger
- article
- Theoretical Computer Science, 2019, 768, pp.91-98. ⟨10.1016/j.tcs.2019.02.022⟩
- Accès au texte intégral et bibtex
-
- titre
- Maehara-style modal nested calculi
- auteur
- Roman Kuznets, Lutz Strassburger
- article
- Archive for Mathematical Logic, 2019, 58 (3-4), pp.359-385. ⟨10.1007/s00153-018-0636-1⟩
- Accès au texte intégral et bibtex
-
- titre
- The problem of proof identity, and why computer scientists should care about Hilbert’s 24th problem
- auteur
- Lutz Strassburger
- article
- Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, 2019, 377 (2140), pp.20180038. ⟨10.1098/rsta.2018.0038⟩
- Accès au bibtex
-
- titre
- Hybrid Linear Logic, revisited
- auteur
- Kaustuv Chaudhuri, Carlos Olarte, Elaine Pimentel, Joëlle Despeyroux
- article
- Mathematical Structures in Computer Science, In press, ⟨10.1017/S0960129518000439⟩
- Accès au texte intégral et bibtex
-
- titre
- A sequent calculus for a semi-associative law
- auteur
- Noam Zeilberger
- article
- Logical Methods in Computer Science, 2019, 15 (1), pp.1-23. ⟨10.23638/LMCS-15(1:9)2019⟩
- Accès au bibtex
-
- titre
- Abstract Machines for Open Call-by-Value
- auteur
- Beniamino Accattoli, Giulio Guerrieri
- article
- Science of Computer Programming, 2019, 184, ⟨10.1016/j.scico.2019.03.002⟩
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Factorization and Normalization, Essentially
- auteur
- Beniamino Accattoli, Claudia Faggian, Giulio Guerrieri
- article
- APLAS 2019 – 17th Asian Symposium on Programming Languages and Systems, Dec 2019, Bali, Indonesia. ⟨10.1007/978-3-030-34175-6_9⟩
- Accès au texte intégral et bibtex
-
- titre
- Crumbling Abstract Machines
- auteur
- Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri, Claudio Sacerdoti Coen
- article
- PPDP 2019 – 21st International Symposium on Principles and Practice of Programming Languages, Oct 2019, Porto, Portugal. ⟨10.1145/3354166.3354169⟩
- Accès au texte intégral et bibtex
-
- titre
- Sharing Equality is Linear
- auteur
- Andrea Condoluci, Beniamino Accattoli, Claudio Sacerdoti Coen
- article
- PPDP 2019 – 21st International Symposium on Principles and Practice of Programming Languages, Oct 2019, Porto, Portugal. ⟨10.1145/3354166.3354174⟩
- Accès au texte intégral et bibtex
-
- titre
- Property-Based Testing via Proof Reconstruction
- auteur
- Roberto Blanco, Dale Miller, Alberto Momigliano
- article
- PPDP 2019 – 21st International Symposium on Principles and Practice of Programming Languages, Oct 2019, Porto, Portugal. pp.1-13, ⟨10.1145/3354166.3354170⟩
- Accès au texte intégral et bibtex
-
- titre
- Functional programming with $λ$-tree syntax
- auteur
- Ulysse Gérard, Dale Miller, Gabriel Scherer
- article
- PPDP 2019 – 21st International Symposium on Principles and Practice of Programming Languages, Oct 2019, Porto, Portugal. pp.1-16, ⟨10.1145/3354166.3354177⟩
- Accès au texte intégral et bibtex
-
- titre
- On Combinatorial Proofs for Modal Logic
- auteur
- Matteo Acclavio, Lutz Strassburger
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- Towards a Combinatorial Proof Theory
- auteur
- Benjamin Ralph, Lutz Strassburger
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- On Combinatorial Proofs for Logics of Relevance and Entailment
- auteur
- Matteo Acclavio, Lutz Strassburger
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- A Fresh Look at the λ-Calculus
- auteur
- Beniamino Accattoli
- article
- FSCD 2019 – 4th International Conference on Formal Structures for Computation and Deduction, Jun 2019, Dortmund, Germany. ⟨10.4230/LIPIcs.FSCD.2019.1⟩
- Accès au texte intégral et bibtex
-
- titre
- Intuitionistic proofs without syntax
- auteur
- Willem Heijltjes, Dominic J D Hughes, Lutz Strassburger
- article
- LICS 2019 – 34th Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2019, Vancouver, Canada. pp.1-13, ⟨10.1109/LICS.2019.8785827⟩
- Accès au texte intégral et bibtex
-
- titre
- Proof Nets for First-Order Additive Linear Logic
- auteur
- Willem Heijltjes, Dominic J D Hughes, Lutz Strassburger
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- Types by Need
- auteur
- Beniamino Accattoli, Giulio Guerrieri, Maico Leberle
- article
- ESOP 2019 – 28th European Symposium on Programming, Apr 2019, Prague, Czech Republic. ⟨10.1007/978-3-030-17184-1_15⟩
- Accès au texte intégral et bibtex
-
- titre
- Unboxing Mutually Recursive Type Definitions in OCaml
- auteur
- Simon Colin, Rodolphe Lepigre, Gabriel Scherer
- article
- JFLA 2019 – 30 èmes journées francophones des langages applicatifs, Jan 2019, Les Rousses, France
- Accès au texte intégral et bibtex
-
- titre
- A Proof-Theoretic Approach to Certifying Skolemization
- auteur
- Kaustuv Chaudhuri, Matteo Manighetti, Dale Miller
- article
- CPP 2019 – 8th ACM SIGPLAN International Conference, Jan 2019, Cascais, Portugal. pp.78-90, ⟨10.1145/3293880.3294094⟩
- Accès au texte intégral et bibtex
-
Lectures
- titre
- Introduction to Deep Inference
- auteur
- Andrea Aler Tubella, Lutz Strassburger
- article
- École thématique. Introduction to Deep Inference, Riga, Latvia. 2019
- Accès au texte intégral et bibtex
-
2018
Conference papers
- titre
- A theory of linear typings as flows on 3-valent graphs
- auteur
- Noam Zeilberger
- article
- 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⟩
- Accès au bibtex
-
- titre
- The Sequent Calculus of Skew Monoidal Categories
- auteur
- Tarmo Uustalu, Niccolò Veltri, Noam Zeilberger
- article
- 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⟩
- Accès au bibtex
-
2012
Books
- titre
- Automated Reasoning: 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 2012, Proceedings
- auteur
- Gramlich Bernhard, Dale Miller, Sattler Uli
- article
- Springer, 7364, pp.1-568, 2012, Lecture Notes in Artificial Intelligence, ⟨10.1007/978-3-642-31365-3⟩
- Accès au bibtex
-
2005
Preprints, Working Papers, …
- titre
- A constructive proof of Skolem theorem for constructive logic
- auteur
- Gilles Dowek, Benjamin Werner
- article
- 2005
- Accès au texte intégral et bibtex
-
2021
Journal articles
- titre
- A fully labelled proof system for intuitionistic modal logics
- auteur
- Sonia Marin, Marianela Morales, Lutz Strassburger
- article
- Journal of Logic and Computation, 2021, 31 (3), pp.998-1022. ⟨10.1093/logcom/exab020⟩
- Accès au texte intégral et bibtex
-
2019
Journal articles
- titre
- A proof theory for model checking
- auteur
- Quentin Heath, Dale Miller
- article
- Journal of Automated Reasoning, 2019, 63 (4), pp.857-885. ⟨10.1007/s10817-018-9475-3⟩
- Accès au texte intégral et bibtex
-
- titre
- Connected chord diagrams and bridgeless maps
- auteur
- Julien Courtiel, Karen Yeats, Noam Zeilberger
- article
- The Electronic Journal of Combinatorics, 2019, 26 (4), pp.1-56. ⟨10.37236/7400⟩
- Accès au texte intégral et bibtex
-
- titre
- Mechanized metatheory revisited
- auteur
- Dale Miller
- article
- Journal of Automated Reasoning, 2019, 63 (3), pp.625-665. ⟨10.1007/s10817-018-9483-3⟩
- Accès au texte intégral et bibtex
-
- titre
- Deep inference and expansion trees for second-order multiplicative linear logic
- auteur
- Lutz Strassburger
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- An Intuitionistic Formula Hierarchy Based on High-School Identities
- auteur
- Taus Brock-Nannestad, Danko Ilik
- article
- Mathematical Logic Quarterly, 2019, 65 (1), pp.57-79. ⟨10.1002/malq.201700047⟩
- Accès au texte intégral et bibtex
-
- titre
- Maehara-style modal nested calculi
- auteur
- Roman Kuznets, Lutz Strassburger
- article
- Archive for Mathematical Logic, 2019, 58 (3-4), pp.359-385. ⟨10.1007/s00153-018-0636-1⟩
- Accès au texte intégral et bibtex
-
- titre
- On the decision problem for MELL
- auteur
- Lutz Strassburger
- article
- Theoretical Computer Science, 2019, 768, pp.91-98. ⟨10.1016/j.tcs.2019.02.022⟩
- Accès au texte intégral et bibtex
-
- titre
- The problem of proof identity, and why computer scientists should care about Hilbert’s 24th problem
- auteur
- Lutz Strassburger
- article
- Philosophical Transactions of the Royal Society A: Mathematical, Physical and Engineering Sciences, 2019, 377 (2140), pp.20180038. ⟨10.1098/rsta.2018.0038⟩
- Accès au bibtex
-
- titre
- Abstract Machines for Open Call-by-Value
- auteur
- Beniamino Accattoli, Giulio Guerrieri
- article
- Science of Computer Programming, 2019, 184, ⟨10.1016/j.scico.2019.03.002⟩
- Accès au texte intégral et bibtex
-
- titre
- Hybrid Linear Logic, revisited
- auteur
- Kaustuv Chaudhuri, Carlos Olarte, Elaine Pimentel, Joëlle Despeyroux
- article
- Mathematical Structures in Computer Science, In press, ⟨10.1017/S0960129518000439⟩
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Factorization and Normalization, Essentially
- auteur
- Beniamino Accattoli, Claudia Faggian, Giulio Guerrieri
- article
- APLAS 2019 – 17th Asian Symposium on Programming Languages and Systems, Dec 2019, Bali, Indonesia. ⟨10.1007/978-3-030-34175-6_9⟩
- Accès au texte intégral et bibtex
-
- titre
- Sharing Equality is Linear
- auteur
- Andrea Condoluci, Beniamino Accattoli, Claudio Sacerdoti Coen
- article
- PPDP 2019 – 21st International Symposium on Principles and Practice of Programming Languages, Oct 2019, Porto, Portugal. ⟨10.1145/3354166.3354174⟩
- Accès au texte intégral et bibtex
-
- titre
- Crumbling Abstract Machines
- auteur
- Beniamino Accattoli, Andrea Condoluci, Giulio Guerrieri, Claudio Sacerdoti Coen
- article
- PPDP 2019 – 21st International Symposium on Principles and Practice of Programming Languages, Oct 2019, Porto, Portugal. ⟨10.1145/3354166.3354169⟩
- Accès au texte intégral et bibtex
-
- titre
- Property-Based Testing via Proof Reconstruction
- auteur
- Roberto Blanco, Dale Miller, Alberto Momigliano
- article
- PPDP 2019 – 21st International Symposium on Principles and Practice of Programming Languages, Oct 2019, Porto, Portugal. pp.1-13, ⟨10.1145/3354166.3354170⟩
- Accès au texte intégral et bibtex
-
- titre
- Functional programming with $λ$-tree syntax
- auteur
- Ulysse Gérard, Dale Miller, Gabriel Scherer
- article
- PPDP 2019 – 21st International Symposium on Principles and Practice of Programming Languages, Oct 2019, Porto, Portugal. pp.1-16, ⟨10.1145/3354166.3354177⟩
- Accès au texte intégral et bibtex
-
- titre
- Towards a Combinatorial Proof Theory
- auteur
- Benjamin Ralph, Lutz Strassburger
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- On Combinatorial Proofs for Modal Logic
- auteur
- Matteo Acclavio, Lutz Strassburger
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- On Combinatorial Proofs for Logics of Relevance and Entailment
- auteur
- Matteo Acclavio, Lutz Strassburger
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- Intuitionistic proofs without syntax
- auteur
- Willem Heijltjes, Dominic J D Hughes, Lutz Strassburger
- article
- LICS 2019 – 34th Annual ACM/IEEE Symposium on Logic in Computer Science, Jun 2019, Vancouver, Canada. pp.1-13, ⟨10.1109/LICS.2019.8785827⟩
- Accès au texte intégral et bibtex
-
- titre
- A Fresh Look at the λ-Calculus
- auteur
- Beniamino Accattoli
- article
- FSCD 2019 – 4th International Conference on Formal Structures for Computation and Deduction, Jun 2019, Dortmund, Germany. ⟨10.4230/LIPIcs.FSCD.2019.1⟩
- Accès au texte intégral et bibtex
-
- titre
- Proof Nets for First-Order Additive Linear Logic
- auteur
- Willem Heijltjes, Dominic J D Hughes, Lutz Strassburger
- article
- 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⟩
- Accès au texte intégral et bibtex
-
- titre
- Types by Need
- auteur
- Beniamino Accattoli, Giulio Guerrieri, Maico Leberle
- article
- ESOP 2019 – 28th European Symposium on Programming, Apr 2019, Prague, Czech Republic. ⟨10.1007/978-3-030-17184-1_15⟩
- Accès au texte intégral et bibtex
-
- titre
- Unboxing Mutually Recursive Type Definitions in OCaml
- auteur
- Simon Colin, Rodolphe Lepigre, Gabriel Scherer
- article
- JFLA 2019 – 30 èmes journées francophones des langages applicatifs, Jan 2019, Les Rousses, France
- Accès au texte intégral et bibtex
-
- titre
- A Proof-Theoretic Approach to Certifying Skolemization
- auteur
- Kaustuv Chaudhuri, Matteo Manighetti, Dale Miller
- article
- CPP 2019 – 8th ACM SIGPLAN International Conference, Jan 2019, Cascais, Portugal. pp.78-90, ⟨10.1145/3293880.3294094⟩
- Accès au texte intégral et bibtex
-
Special issue
- titre
- Preface
- auteur
- Beniamino Accattoli, Carlos Olarte
- article
- Beniamino Accattoli; Carlos Olarte. Electronic Notes in Theoretical Computer Science, 344, pp.1-2, 2019, The proceedings of LSFA 2018, the 13th Workshop on Logical and Semantic Frameworks with Applications (LSFA’18), ⟨10.1016/j.entcs.2019.07.001⟩
- Accès au bibtex
-
Lectures
- titre
- Introduction to Deep Inference
- auteur
- Andrea Aler Tubella, Lutz Strassburger
- article
- École thématique. Introduction to Deep Inference, Riga, Latvia. 2019
- Accès au texte intégral et bibtex
-
2018
Journal articles
- titre
- Capturing the Future by Replaying the Past Functional Pearl
- auteur
- James Koppel, Gabriel Scherer, Armando Solar-Lezama
- article
- Proceedings of the ACM on Programming Languages, 2018, 2 (ICFP), pp.1 – 29. ⟨10.1145/3236771⟩
- Accès au texte intégral et bibtex
-
- titre
- Merlin: a language server for OCaml (experience report)
- auteur
- Frédéric Bour, Thomas Réfis, Gabriel Scherer
- article
- Proceedings of the ACM on Programming Languages, 2018, 2 (ICFP), pp.1 – 15. ⟨10.1145/3236798⟩
- Accès au texte intégral et bibtex
-
- titre
- Proof Diagrams for Multiplicative Linear Logic: Syntax and Semantics
- auteur
- Matteo Acclavio
- article
- Journal of Automated Reasoning, 2018, ⟨10.1007/s10817-018-9466-4⟩
- Accès au bibtex
-
- titre
- Expressing Additives Using Multiplicatives and Subexponentials
- auteur
- Kaustuv Chaudhuri
- article
- Mathematical Structures in Computer Science, 2018, 28 (5), pp.651-666
- Accès au texte intégral et bibtex
-
- titre
- Correctness of Speculative Optimizations with Dynamic Deoptimization
- auteur
- Olivier Flückiger, Gabriel Scherer, Ming-Ho Yee, Aviral Goel, Amal Ahmed, Jan Vitek
- article
- Proceedings of the ACM on Programming Languages, 2018, 2 (POPL), ⟨10.1145/3158137⟩
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Types of Fireballs
- auteur
- Beniamino Accattoli, Giulio Guerrieri
- article
- APLAS 2018 – 16th Asian Symposium on Programming Languages and System, Dec 2018, Wellington, New Zealand
- Accès au texte intégral et bibtex
-
- titre
- Proof Nets and the Linear Substitution Calculus
- auteur
- Beniamino Accattoli
- article
- 15th International Colloquium on Theoretical Aspects of Computing (ICTAC 2018), Oct 2018, Stellenbosch, South Africa
- Accès au texte intégral et bibtex
-
- titre
- A preview of a tutorial on L (polarized μμ-tilde)
- auteur
- Kenji Maillard, Étienne Miquey, Xavier Montillet, Guillaume Munch-Maccagnoni, Gabriel Scherer
- article
- HOPE 2018 – 7th ACM SIGPLAN Workshop on Higher-Order Programming with Effects, Sep 2018, St. Louis, United States
- Accès au bibtex
-
- titre
- Tight typings and split bounds
- auteur
- Beniamino Accattoli, Stéphane Graham-Lengrand, Delia Kesner
- article
- 23rd ACM International Conference on Functional Programming, Sep 2018, St Louis, United States. pp.1 – 30, ⟨10.1145/3236789⟩
- Accès au texte intégral et bibtex
-
- titre
- Admissible Tools in the Kitchen of Intuitionistic Logic
- auteur
- Andrea Condoluci, Matteo Manighetti
- article
- Seventh International Workshop on Classical Logic and Computation (CL&C 2018), Jul 2018, Oxford, United Kingdom. pp.10-23
- Accès au texte intégral et bibtex
-
- titre
- Functional programming with λ$-tree$ syntax: a progress report
- auteur
- Ulysse Gérard, Dale Miller
- article
- 13th international Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Jul 2018, Oxford, United Kingdom
- Accès au texte intégral et bibtex
-
- titre
- Computation-as-deduction in Abella: work in progress
- auteur
- Kaustuv Chaudhuri, Ulysse Gérard, Dale Miller
- article
- 13th international Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Jul 2018, Oxford, United Kingdom
- Accès au texte intégral et bibtex
-
- titre
- Centralizing equality reasoning in MCSAT
- auteur
- François Bobot, Stéphane Graham-Lengrand, Bruno Marre, Guillaume Bury
- article
- 16th International Workshop on Satisfiability Modulo Theories (SMT 2018), Jul 2018, Oxford, United Kingdom
- Accès au texte intégral et bibtex
-
- titre
- Technical specification IEC TS 62989:2018 – Primary optics for concentrator photovoltaic systems
- auteur
- Thomas Arndt, Steve Askins, Jaione Bengoechea, Sam Carter, César Dominguez, Rebeca Herrero, Thorsten Hornung, Hideto Kasai, Rene Kogler, Ralf Leutz, David Miller, Peter Nitz, Steve Scott, Marta Victoria, Philippe Voarino
- article
- CPV-14 – 14th International Conference on Concentrator Photovoltaic Systems, Apr 2018, Puertollano, Spain. pp.070002, ⟨10.1063/1.5053528⟩
- Accès au bibtex
-
- titre
- FabULous Interoperability for ML and a Linear Language
- auteur
- Gabriel Scherer, Max New, Nick Rioux, Amal Ahmed
- article
- International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), Apr 2018, Thessaloniki, Greece. ⟨10.1007/978-3-319-89366-2_8⟩
- Accès au texte intégral et bibtex
-
- titre
- Guiding SMT solvers with Monte Carlo Tree Search and neural networks
- auteur
- Stéphane Graham-Lengrand, Michael Färber
- article
- Third Conference on Artificial Intelligence and Theorem Proving (AITP’2018), Mar 2018, Aussois, France
- Accès au texte intégral et bibtex
-
- titre
- Génération aléatoire de programmes guidée par la vivacité
- auteur
- Gergö Barany, Gabriel Scherer
- article
- JFLA 2018 – Journées Francophones des Langages Applicatifs, Jan 2018, Banyuls-sur-Mer, France
- Accès au texte intégral et bibtex
-
- titre
- A Two-Level Logic Perspective on (Simultaneous) Substitutions
- auteur
- Kaustuv Chaudhuri
- article
- CPP 2018 – Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Jan 2018, Los Angeles, United States
- Accès au texte intégral et bibtex
-
- titre
- Proofs in conflict-driven theory combination
- auteur
- Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar
- article
- Proceedings of the 7th International Conference on Certified Programs and Proofs (CPP’18), Jan 2018, Los Angeles, United States. ⟨10.1145/3167096⟩
- Accès au texte intégral et bibtex
-
Book sections
- titre
- From Syntactic Proofs to Combinatorial Proofs
- auteur
- Matteo Acclavio, Lutz Strassburger
- article
- International Joint Conference on Automated Reasoning, IJCAR 2018, Springer, pp.481-497, 2018, 978-3-319-94204-9
- Accès au texte intégral et bibtex
-
Documents associated with scientific events
- titre
- Influences between logic programming and proof theory
- auteur
- Dale Miller
- article
- HaPoP 2018: Fourth Symposium on the History and Philosophy of Programming, Mar 2018, Oxford, United Kingdom
- Accès au texte intégral et bibtex
-
Reports
- titre
- On the Decision Problem for MELL
- auteur
- Lutz Strassburger
- article
- [Research Report] 9203, Inria Saclay Ile de France. 2018
- Accès au texte intégral et bibtex
-
- titre
- Proof nets for first-order additive linear logic
- auteur
- Willem Heijltjes, Dominic J D Hughes, Lutz Strassburger
- article
- [Research Report] RR-9201, Inria. 2018
- Accès au texte intégral et bibtex
-
2017
Journal articles
- titre
- Perspectives for proof unwinding by programming languages techniques
- auteur
- Danko Ilik
- article
- IfColog Journal of Logics and their Applications (FLAP), 2017, 4 (10), pp.3487-3508
- Accès au texte intégral et bibtex
-
- titre
- On the Value of Variables
- auteur
- Beniamino Accattoli, Claudio Sacerdoti Coen
- article
- Information and Computation, 2017, 255, pp.224 – 242. ⟨10.1016/j.ic.2017.01.003⟩
- Accès au texte intégral et bibtex
-
- titre
- Proof Checking and Logic Programming
- auteur
- Dale Miller
- article
- Formal Aspects of Computing, 2017, 29 (3), pp.383-399 ⟨10.1007/s00165-016-0393-z⟩
- Accès au texte intégral et bibtex
-
- titre
- A Semantic Framework for Proof Evidence
- auteur
- Zakaria Chihani, Dale Miller, Fabien Renaud
- article
- Journal of Automated Reasoning, 2017, 59 (3), pp.287-330. ⟨10.1007/s10817-016-9380-6⟩
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- The Negligible and Yet Subtle Cost of Pattern Matching
- auteur
- Beniamino Accattoli, Bruno Barras
- article
- Programming Languages and Systems – 15th Asian Symposium, Nov 2017, Suzhou, China
- Accès au texte intégral et bibtex
-
- titre
- Environments and the Complexity of Abstract Machines.
- auteur
- Beniamino Accattoli, Bruno Barras
- article
- The 19th International Symposium on Principles and Practice of Declarative Programming, Oct 2017, Namur, Belgium. ⟨10.1145/3131851.3131855⟩
- Accès au texte intégral et bibtex
-
- titre
- Proof theory for indexed nested sequents
- auteur
- Sonia Marin, Lutz Strassburger
- article
- TABLEAUX 2017 – Automated Reasoning with Analytic Tableaux and Related Methods, Sep 2017, Brasilia, Brazil. pp.81-97
- Accès au texte intégral et bibtex
-
- titre
- Property-Based Testing via Proof Reconstruction Work-in-progress
- auteur
- Roberto Blanco, Dale Miller, Alberto Momigliano
- article
- LFMTP 17: Logical Frameworks and Meta-Languages: Theory and Practice, Sep 2017, Oxford, United Kingdom
- Accès au texte intégral et bibtex
-
- titre
- Linear logic as a logical framework
- auteur
- Dale Miller
- article
- Proceedings of Structures and Deduction (SD) 2017, Sep 2017, Oxford, United Kingdom
- Accès au bibtex
-
- titre
- Using linear logic and proof theory to unify computational logic
- auteur
- Dale Miller
- article
- Proceedings of Trends in Linear Logic and Applications (TLLA 17), Sep 2017, Oxford, United Kingdom
- Accès au texte intégral et bibtex
-
- titre
- Combinatorial Flows and their Normalisation
- auteur
- Lutz Strassburger
- article
- FSCD 2017 – 2nd International Conference on Formal Structures for Computation and Deduction, Sep 2017, Oxford, United Kingdom. pp.311 – 3117, ⟨10.4230/LIPIcs.FSCD.2017.31⟩
- Accès au texte intégral et bibtex
-
- titre
- Separating Functional Computation from Relations
- auteur
- Ulysse Gérard, Dale Miller
- article
- 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), Aug 2017, Stockholm, Sweden. pp.23:1–23:17
- Accès au texte intégral et bibtex
-
- titre
- Satisfiability Modulo Theories and Assignments
- auteur
- Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar
- article
- CADE 2017 – 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden. ⟨10.1007/978-3-319-63046-5_4⟩
- Accès au texte intégral et bibtex
-
- titre
- Translating Between Implicit and Explicit Versions of Proof
- auteur
- Roberto Blanco, Zakaria Chihani, Dale Miller
- article
- CADE 26 – 26th International Conference on Automated Deduction, Aug 2017, Gothenburg, Sweden
- Accès au texte intégral et bibtex
-
- titre
- An MCSAT treatment of Bit-Vectors (preliminary report)
- auteur
- Stéphane Graham-Lengrand, Dejan Jovanović
- article
- SMT 2017 – 15th International Workshop on Satisfiability Modulo Theories, Jul 2017, Heidelberg, Germany
- Accès au texte intégral et bibtex
-
- titre
- On the Length of Medial-Switch-Mix Derivations
- auteur
- Paola Bruscoli, Lutz Strassburger
- article
- WoLLIC 2017 – Logic, Language, Information, and Computation, Jul 2017, London, United Kingdom
- Accès au texte intégral et bibtex
-
- titre
- Implementing Open Call-by-Value
- auteur
- Beniamino Accattoli, Giulio Guerrieri
- article
- 7th International Conference on Fundamentals of Software Engineering (FSEN), Apr 2017, Teheran, Iran. pp.1-19, ⟨10.1007/978-3-319-68972-2_1⟩
- Accès au texte intégral et bibtex
-
- titre
- On the exp-log normal form of types
- auteur
- Danko Ilik
- article
- Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, Jan 2017, Paris, France. pp.387-399
- Accès au texte intégral et bibtex
-
- titre
- Deciding equivalence with sums and the empty type
- auteur
- Gabriel Scherer
- article
- POPL 2017, Jan 2017, Paris, France
- Accès au texte intégral et bibtex
-
- titre
- Typeful Continuations
- auteur
- Matthias Puech
- article
- JFLA 2017 – 28ème Journées Francophones des Langages Applicatifs, Jan 2017, Gourette, France. pp.1-14
- Accès au texte intégral et bibtex
-
- titre
- Mechanized Metatheory Revisited: An Extended Abstract
- auteur
- Dale Miller
- article
- Post-proceedings of TYPES 2016 , 2017, Novi Sad, Serbia. ⟨10.4230/LIPIcs⟩
- Accès au texte intégral et bibtex
-
Documents associated with scientific events
- titre
- Justification logic for constructive modal logic *
- auteur
- Roman Kuznets, Sonia Marin, Lutz Strassburger
- article
- IMLA 2017 – 7th Workshop on Intuitionistic Modal Logic and Applications, Jul 2017, Toulouse, France. , 2017
- Accès au texte intégral et bibtex
-
Proceedings
- titre
- 2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017)
- auteur
- Dale Miller
- article
- Dale Miller. FSCD 2017 – 2nd International Conference on Formal Structures for Computation and Deduction , Sep 2017, Oxford, United Kingdom. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, 2017, 978-3-95977-047-7
- Accès au bibtex
-
Reports
- titre
- Maehara-style Modal Nested Calculi
- auteur
- Lutz Strassburger, Roman Kuznets
- article
- [Research Report] RR-9123, Inria Saclay. 2017
- Accès au texte intégral et bibtex
-
- titre
- Deep Inference, Expansion Trees, and Proof Graphs for Second Order Propositional Multiplicative Linear Logic
- auteur
- Lutz Strassburger
- article
- [Research Report] RR-9071, Inria Saclay Ile de France. 2017, pp.38
- Accès au texte intégral et bibtex
-
- titre
- On the Proof Theory of Indexed Nested Sequents for Classical and Intuitionistic Modal Logics
- auteur
- Sonia Marin, Lutz Strassburger
- article
- [Research Report] RR-9061, Inria. 2017
- Accès au texte intégral et bibtex
-
- titre
- Combinatorial Flows and Proof Compression
- auteur
- Lutz Strassburger
- article
- [Research Report] RR-9048, Inria Saclay. 2017
- Accès au texte intégral et bibtex
-
2016
Journal articles
- titre
- On linear rewriting systems for Boolean logic and some applications to proof theory
- auteur
- Anupam Das, Lutz Strassburger
- article
- Logical Methods in Computer Science, 2016
- Accès au bibtex
-
- titre
- Linear lambda terms as invariants of rooted trivalent maps
- auteur
- Noam Zeilberger
- article
- Journal of Functional Programming, 2016, 26, ⟨10.1017/S095679681600023X⟩
- Accès au bibtex
-
- titre
- Preserving differential privacy under finite-precision semantics
- auteur
- Ivan Gazeau, Dale Miller, Catuscia Palamidessi
- article
- Theoretical Computer Science, 2016
- Accès au texte intégral et bibtex
-
- titre
- (Leftmost-outermost) beta reduction is invariant, indeed
- auteur
- Beniamino Accattoli, Ugo Dal Lago
- article
- Logical Methods in Computer Science, 2016, ⟨10.2168/LMCS-12(1:4)2016⟩
- Accès au texte intégral et bibtex
-
- titre
- Proof Certificates for Equality Reasoning
- auteur
- Zakaria Chihani, Dale Miller
- article
- Electronic Notes in Theoretical Computer Science, 2016, 323, pp.93 – 108. ⟨10.1016/j.entcs.2016.06.007⟩
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Non-crossing Tree Realizations of Ordered Degree Sequences
- auteur
- Laurent Mehats, Lutz Strassburger
- article
- LACL 2016 – 9th International Conference Logical Aspects of Computational Linguistics – Celebrating 20 Years of LACL (1996–2016), Dec 2016, Nancy, France. ⟨10.1007/978-3-662-53826-5_13⟩
- Accès au bibtex
-
- titre
- Open Call-by-Value
- auteur
- Beniamino Accattoli, Giulio Guerrieri
- article
- 14th Asian Symposium on Programming Languages and Systems (APLAS), Nov 2016, Hanoi, Vietnam. pp.206 – 226, ⟨10.1007/978-3-319-47958-3_12⟩
- Accès au texte intégral et bibtex
-
- titre
- Certification of Prefixed Tableau Proofs for Modal Logic
- auteur
- Tomer Libal, Marco Volpe
- article
- the Seventh International Symposium on Games, Automata, Logics and Formal Verification (GandALF 2016), Sep 2016, Catania, Italy. pp.257 – 271, ⟨10.4204/EPTCS.226.18⟩
- Accès au texte intégral et bibtex
-
- titre
- A focused framework for emulating modal proof systems
- auteur
- Sonia Marin, Dale Miller, Marco Volpe
- article
- 11th conference on “Advances in Modal Logic”, Aug 2016, Budapest, Hungary. pp.469-488
- Accès au texte intégral et bibtex
-
- titre
- The Useful MAM, a Reasonable Implementation of the Strong $\lambda$-Calculus
- auteur
- Beniamino Accattoli
- article
- 23rd International Workshop on Logic, Language, Information, and Computation (WoLLIC 2016), Aug 2016, Puebla, Mexico. pp.1 – 21, ⟨10.1007/978-3-662-52921-8_1⟩
- Accès au texte intégral et bibtex
-
- titre
- Towards a Substitution Tree Based Index for Higher-order Resolution Theorem Provers
- auteur
- Tomer Libal, Alexander Steen
- article
- 5th Workshop on Practical Aspects of Automated Reasoning, Jul 2016, Coimbra, Portugal
- Accès au texte intégral et bibtex
-
- titre
- The Complexity of Abstract Machines
- auteur
- Beniamino Accattoli
- article
- Third International Workshop on Rewriting Techniques for Program Transformations and Evaluation (WPTE 2016), Jun 2016, Porto, Portugal. pp.1 – 15, ⟨10.4204/EPTCS.235.1⟩
- Accès au texte intégral et bibtex
-
- titre
- Modular Focused Proof Systems for Intuitionistic Modal Logics
- auteur
- Kaustuv Chaudhuri, Sonia Marin, Lutz Strassburger
- article
- FSCD 2016 – 1st International Conference on Formal Structures for Computation and Deduction, Jun 2016, Porto, Portugal. ⟨10.4230/LIPIcs.FSCD.2016.16⟩
- Accès au bibtex
-
- titre
- Functions-as-constructors Higher-order Unification
- auteur
- Tomer Libal, Dale Miller
- article
- 1st International Conference on Formal Structures for Computation and Deduction (FSCD 2016), Delia Kesner and Brigitte Pientka, Jun 2016, Porto, Portugal. pp.1 – 17, ⟨10.4230/LIPIcs.FSCD.2016.26⟩
- Accès au texte intégral et bibtex
-
- titre
- A bifibrational reconstruction of Lawvere’s presheaf hyperdoctrine
- auteur
- Paul-André Melliès, Noam Zeilberger
- article
- IEEE/ACM Logic in Computer Science (LICS) 2016, Jun 2016, New York, United States
- Accès au bibtex
-
- titre
- Proving Determinacy of the PharOS Real-Time Operating System
- auteur
- Selma Azaiez, Damien Doligez, Matthieu Lemerre, Tomer Libal, Stephan Merz
- article
- Abstract State Machines, Alloy, B, TLA, VDM, and Z – 5th International Conference, ABZ 2016, May 2016, Linz, Austria. pp.70-85, ⟨10.1007/978-3-319-33600-8_4⟩
- Accès au texte intégral et bibtex
-
- titre
- Focused and Synthetic Nested Sequents
- auteur
- Kaustuv Chaudhuri, Sonia Marin, Lutz Strassburger
- article
- FOSSACS 2016 – 19th International Conference Foundations of Software Science and Computation Structures, Apr 2016, Eindhoven, Netherlands. ⟨10.1007/978-3-662-49630-5_23⟩
- Accès au bibtex
-
- titre
- Space-efficient Planar Acyclicity Constraints – A Declarative Pearl
- auteur
- Taus Brock-Nannestad
- article
- FLOPS 2016 – 13th International Symposium on Functional and Logic Programming, Mar 2016, Kochi, Japan
- Accès au texte intégral et bibtex
-
Reports
- titre
- A model-constructing framework for theory combination
- auteur
- Maria Paola Bonacina, Stéphane Graham-Lengrand, Natarajan Shankar
- article
- [Research Report] RR-99/2016, Universita degli Studi di Verona. 2016
- Accès au bibtex
-
- titre
- Focused and Synthetic Nested Sequents (Extended Technical Report)
- auteur
- Kaustuv Chaudhuri, Sonia Marin, Lutz Strassburger
- article
- [Research Report] Inria. 2016
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, …
- titre
- An interactive assistant for the definition of proof certificates
- auteur
- Roberto Blanco, Zakaria Chihani
- article
- 2016
- Accès au texte intégral et bibtex
-
- titre
- Classical polarizations yield double-negation translations
- auteur
- Zakaria Chihani, Danko Ilik, Dale Miller
- article
- 2016
- Accès au texte intégral et bibtex
-
2015
Journal articles
- titre
- On Nested Sequents for Constructive Modal Logics
- auteur
- Ryuta Arisaka, Anupam Das, Lutz Strassburger
- article
- Logical Methods in Computer Science, 2015, 11 (3), pp.1-33. ⟨10.2168/LMCS-11(3:7)2015⟩
- Accès au texte intégral et bibtex
-
- titre
- On the Power of Substitution in the Calculus of Structures
- auteur
- Lutz Strassburger, Novak Novakovic
- article
- ACM Transactions on Computational Logic, 2015, 16 (3), ⟨10.1145/2701424⟩
- Accès au bibtex
-
- titre
- Proof nets and the call-by-value λ-calculus
- auteur
- Beniamino Accattoli
- article
- Theoretical Computer Science, 2015, ⟨10.1016/j.tcs.2015.08.006⟩
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- A Strong Distillery
- auteur
- Beniamino Accattoli, Pablo Barenbaum, Damiano Mazza
- article
- Programming Languages and Systems – 13th Asian Symposium, APLAS 2015, Nov 2015, Pohang, South Korea. pp.231-250, ⟨10.1007/978-3-319-26529-2_13⟩
- Accès au texte intégral et bibtex
-
- titre
- On Subexponentials, Synthetic Connectives, and Multi-level Delimited Control
- auteur
- Chuck Liang, Dale Miller
- article
- LPAR 20 – International Conference on Logic for Programming, Artificial Intelligence and Reasoning, Nov 2015, Suva, Fiji. pp.297-312, ⟨10.1007/978-3-662-48899-7_21⟩
- Accès au texte intégral et bibtex
-
- titre
- An adequate compositional encoding of bigraph structure in linear logic with subexponentials
- auteur
- Kaustuv Chaudhuri, Giselle Reis
- article
- 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Nov 2015, Suva, Fiji. pp.146–161, ⟨10.1007/978-3-662-48899-7_11⟩
- Accès au texte intégral et bibtex
-
- titre
- Focused labeled proof systems for modal logic
- auteur
- Dale Miller, Marco Volpe
- article
- 20th International Conference on Logic for Programming, Artificial Intelligence and Reasoning (LPAR), Nov 2015, Suva, Fiji
- Accès au texte intégral et bibtex
-
- titre
- Defining the meaning of TPTP formatted proofs
- auteur
- Roberto Blanco, Tomer Libal, Dale Miller
- article
- 11th International Workshop on the Implementation of Logics, Nov 2015, Suva, Fiji
- Accès au texte intégral et bibtex
-
- titre
- Proof Outlines as Proof Certificates: A System Description
- auteur
- Roberto Blanco, Dale Miller
- article
- First International Workshop on Focusing, Nov 2015, Suva, Fiji
- Accès au texte intégral et bibtex
-
- titre
- Realisability semantics of abstract focussing, formalised
- auteur
- Stéphane Graham-Lengrand
- article
- Proceedings of the First International Workshop on Focusing, Nov 2015, Suva, Fiji. pp.14, ⟨10.4204/EPTCS.197.3⟩
- Accès au bibtex
-
- titre
- The Proof Certifier Checkers
- auteur
- Zakaria Chihani, Tomer Libal, Giselle Reis
- article
- Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), Sep 2015, Wroclaw, Poland. pp.201-210, ⟨10.1007/978-3-319-24312-2_14⟩
- Accès au texte intégral et bibtex
-
- titre
- Disproving Using the Inverse Method by Iterative Refinement of Finite Approximations
- auteur
- Taus Brock-Nannestad, Kaustuv Chaudhuri
- article
- Automated Reasoning with Analytic Tableaux and Related Methods, Sep 2015, Wrocław, Poland. ⟨10.1007/978-3-319-24312-2_11⟩
- Accès au texte intégral et bibtex
-
- titre
- Axiomatic constraint systems for proof search modulo theories
- auteur
- Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand, Jean-Marc Notin, Assia Mahboubi
- article
- 10th International Symposium on Frontiers of Combining Systems (FroCoS’15), Sep 2015, Wroclaw, Poland. ⟨10.1007/978-3-319-24246-0_14⟩
- Accès au bibtex
-
- titre
- Importing SMT and Connection proofs as expansion trees
- auteur
- Giselle Reis
- article
- PxTP 2015 – Proceedings Fourth Workshop on Proof eXchange for Theorem Proving, Aug 2015, Berlin, Germany. ⟨10.4204/EPTCS.186.3⟩
- Accès au texte intégral et bibtex
-
- titre
- A framework for proof certificates in finite state exploration
- auteur
- Quentin Heath, Dale Miller
- article
- Proceedings of the Fourth Workshop on Proof eXchange for Theorem Proving, Aug 2015, Berlin, Germany. ⟨10.4204/EPTCS.186.4⟩
- Accès au texte intégral et bibtex
-
- titre
- Regular Patterns in Second-Order Unification
- auteur
- Tomer Libal
- article
- Proceedings of CADE-25 – 25th International Conference on Automated Deduction, Berlin, Germany, Aug 2015, Berlin, Germany. ⟨10.1007/978-3-319-21401-6_38⟩
- Accès au bibtex
-
- titre
- Slot Machines: an approach to the Strategy Challenge in SMT solving (presentation only)
- auteur
- Stéphane Graham-Lengrand
- article
- 13th International Workshop on Satisfiability Modulo Theories, Jul 2015, San Francisco, United States
- Accès au texte intégral et bibtex
-
- titre
- Computation in Focused Intuitionistic Logic
- auteur
- Taus Brock-Nannestad, Nicolas Guenot, Daniel Gustafsson
- article
- 17th International Symposium on Principles and Practice of Declarative Programming, Jul 2015, Siena, Italy. ⟨10.1145/2790449.2790528⟩
- Accès au texte intégral et bibtex
-
- titre
- On the Relative Usefulness of Fireballs
- auteur
- Beniamino Accattoli, Claudio Sacerdoti Coen
- article
- 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Jul 2015, Kyoto, Japan. ⟨10.1109/LICS.2015.23⟩
- Accès au texte intégral et bibtex
-
- titre
- A Note on the Complexity of Classical and Intuitionistic Proofs
- auteur
- Matthias Baaz, Alexander Leitsch, Giselle Reis
- article
- LICS 2015 – 30th Annual ACM/IEEE Symposium on Logic in Computer Science, Jul 2015, Kyoto, Japan. pp.657 – 666, ⟨10.1109/LICS.2015.66⟩
- Accès au texte intégral et bibtex
-
- titre
- A Proof-theoretic Characterization of Independence in Type Theory
- auteur
- Yuting Wang, Kaustuv Chaudhuri
- article
- 13th International Conference on Typed Lambda Calculi and Applications (TLCA 2015), Jul 2015, Warsaw, Poland. pp.332–346, ⟨10.4230/LIPIcs.TLCA.2015.332⟩
- Accès au texte intégral et bibtex
-
- titre
- No complete linear term rewriting system for propositional logic
- auteur
- Anupam Das, Lutz Strassburger
- article
- 26th International Conference on Rewriting Techniques and Applications (RTA 2015), Jun 2015, Warsaw, Poland. ⟨10.4230/LIPIcs.RTA.2015.127⟩
- Accès au texte intégral et bibtex
-
- titre
- Towards Deciding Second-order Unification Problems Using Regular Tree Automata
- auteur
- Tomer Libal
- article
- 29th International Workshop on Unification, Jun 2015, Warsaw, Poland
- Accès au texte intégral et bibtex
-
- titre
- Focused Linear Logic and the λ-calculus
- auteur
- Taus Brock-Nannestad, Nicolas Guenot
- article
- Mathematical Foundations of Programming Semantics XXXI, Jun 2015, Nijmegen, Netherlands. ⟨10.1016/j.entcs.2015.12.008⟩
- Accès au texte intégral et bibtex
-
- titre
- A Lightweight Formalization of the Metatheory of Bisimulation-Up-To
- auteur
- Kaustuv Chaudhuri, Matteo Cimini, Dale Miller
- article
- 4th ACM-SIGPLAN Conference on Certified Programs and Proofs (CPP), ACM-SIGPLAN, Jan 2015, Mumbai, India. ⟨10.1145/2676724.2693170⟩
- Accès au texte intégral et bibtex
-
Book sections
- titre
- Foundational Proof Certificates
- auteur
- Dale Miller
- article
- David Delahaye and Bruno Woltzenlogel Paleo. All about Proofs, Proofs for All, Mathematical Logic and Foundations (55), College Publications, pp.150-163, 2015, All about Proofs, Proofs for All, 978-1-84890-166-7
- Accès au bibtex
-
Books
- titre
- Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice
- auteur
- Iliano Cervesato, Kaustuv Chaudhuri
- article
- Iliano Cervesato; Kaustuv Chaudhuri. , 2015, ⟨10.4204/EPTCS.185⟩
- Accès au bibtex
-
Documents associated with scientific events
- titre
- Reasoning about Computational Systems using Abella
- auteur
- Kaustuv Chaudhuri, Gopalan Nadathur
- article
- Abella Tutorial, Aug 2015, Berlin, Germany. 2015
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, …
- titre
- An interpolation-based method for the verification of security protocols
- auteur
- Marco Rocchetto, Luca Viganò, Marco Volpe
- article
- 2015
- Accès au texte intégral et bibtex
-
- titre
- A Branching Distributed Temporal Logic for Reasoning about Quantum State Transformations
- auteur
- Luca Viganò, Marco Volpe, Margherita Zorzi
- article
- 2015
- Accès au texte intégral et bibtex
-
2014
Journal articles
- titre
- A Direct Version of Veldman’s Proof of Open Induction on Cantor Space via Delimited Control Operators
- auteur
- Danko Ilik, Keiko Nakata
- article
- Leibniz International Proceedings in Informatics , 2014, pp.288-201. ⟨10.4230/LIPIcs.TYPES.2013.188⟩
- Accès au texte intégral et bibtex
-
- titre
- Proof nets and semi-star-autonomous categories
- auteur
- Willem Heijltjes, Lutz Strassburger
- article
- Mathematical Structures in Computer Science, 2014, 26 (5), pp.1-40. ⟨10.1017/S0960129514000395⟩
- Accès au texte intégral et bibtex
-
- titre
- Vitamin D as an early predictor of multiple sclerosis activity and progression.
- auteur
- Alberto Ascherio, Kassandra L. Munger, Rick White, Karl Köchert, Kelly Claire Simon, Chris H. Polman, Mark S. Freedman, Hans-Peter Hartung, David H. Miller, Xavier Montalbán, Gilles Edan, Frederik Barkhof, Dirk Pleimes, Ernst-Wilhelm Radü, Rupert Sandbrink, Ludwig Kappos, Christoph Pohl
- article
- JAMA neurology, 2014, pp.306-14
- Accès au bibtex
-
- titre
- Interferon beta-1b reduces black holes in a randomised trial of clinically isolated syndrome.
- auteur
- Gijsbert J A Nagtegaal, Christoph Pohl, Mike P. Wattjes, Hanneke E. Hulst, Mark S. Freedman, Hans-Peter Hartung, David Miller, Xavier Montalbán, Ludwig Kappos, Gilles Edan, Dirk Pleimes, Karola Beckman, Brigitte Stemper, Christoph H. Polman, Rupert Sandbrink, Frederik Barkhof
- article
- Multiple Sclerosis Journal, 2014, 20 (2), pp.234-42
- Accès au bibtex
-
- titre
- Modeling Martin Löf Type Theory in Categories
- auteur
- François Lamarche
- article
- Journal of Applied Logic, 2014, 12 (1), pp.28-44. ⟨10.1016/j.jal.2013.08.003⟩
- Accès au texte intégral et bibtex
-
- titre
- A Multi-Focused Proof System Isomorphic to Expansion Proofs
- auteur
- Kaustuv Chaudhuri, Stefan Hetzl, Dale Miller
- article
- Journal of Logic and Computation, 2014
- Accès au texte intégral et bibtex
-
- titre
- Abella: A System for Reasoning about Relational Specifications
- auteur
- David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan Nadathur, Alwen Tiu, Yuting Wang
- article
- Journal of Formalized Reasoning, 2014, Special Issue: User Tutorials 2, 7 (2), pp.1-89. ⟨10.6092/issn.1972-5787/4650⟩
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- A Two-Level Logic Approach to Reasoning about Typed Specification Languages
- auteur
- Mary Southern, Kaustuv Chaudhuri
- article
- 34th International Conference on Foundation of Software Technology and Theoretical Computer Science (FSTTCS 2014), Dec 2014, New Delhi, India. ⟨10.4230/LIPIcs.FSTTCS.2014.557⟩
- Accès au texte intégral et bibtex
-
- titre
- Parametricity and Proving Free Theorems for Functional-Logic Languages
- auteur
- Stefan Mehner, Daniel Seidel, Lutz Strassburger, Janis Voigtländer
- article
- Principles and Practice of Declarative Programming, PPDP 2014, Sep 2014, Canterbury, United Kingdom. ⟨10.1145/2643135.2643147⟩
- Accès au texte intégral et bibtex
-
- titre
- Label-free Modular Systems for Classical and Intuitionistic Modal Logics
- auteur
- Sonia Marin, Lutz Strassburger
- article
- Advances in Modal Logic 10, Aug 2014, Groningen, Netherlands
- Accès au texte intégral et bibtex
-
- titre
- Automatically Deriving Schematic Theorems for Dynamic Contexts
- auteur
- Olivier Savary Bélanger, Kaustuv Chaudhuri
- article
- Logical Frameworks and Meta-Languages: Theory and Practice, Jul 2014, Vienna, Austria. ⟨10.1145/2631172.2631181⟩
- Accès au texte intégral et bibtex
-
- titre
- Symmetric Normalisation for Intuitionistic Logic
- auteur
- Nicolas Guenot, Lutz Strassburger
- article
- CSL-LICS 2014, Jul 2014, Vienna, Austria. ⟨10.1145/2603088.2603160⟩
- Accès au texte intégral et bibtex
-
- titre
- Axioms and Decidability for Type Isomorphism in the Presence of Sums
- auteur
- Danko Ilik
- article
- CSL-LICS ’14 Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), SIGLOG ACM Special Interest Group on Logic and Computation; EACSL European Association for Computer Science Logic; IEEE-CS – DATC IEEE Computer Society, Jul 2014, Vienna, Austria. ⟨10.1145/2603088.2603115⟩
- Accès au texte intégral et bibtex
-
- titre
- On the pigeonhole and related principles in deep inference and monotone systems
- auteur
- Anupam Das
- article
- CSL-LICS ’14 Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS), Jul 2014, Vienna, Austria. pp.1 – 10, ⟨10.1145/2603088.2603164⟩
- Accès au texte intégral et bibtex
-
- titre
- Equality and fixpoints in the calculus of structures
- auteur
- Kaustuv Chaudhuri, Nicolas Guenot
- article
- JOINT MEETING OF the Twenty-Third EACSL Annual Conference on COMPUTER SCIENCE LOGIC (CSL) AND the Twenty-Ninth Annual ACM/IEEE Symposium on LOGIC IN COMPUTER SCIENCE (LICS), Jul 2014, Vienna, Austria. pp.1 – 10, ⟨10.1145/2603088.2603140⟩
- Accès au texte intégral et bibtex
-
- titre
- Undecidability of Multiplicative Subexponential Logic
- auteur
- Kaustuv Chaudhuri
- article
- Proceedings of the Third International Workshop on Linearity, Jul 2014, Vienna, Austria. pp.1–8, ⟨10.4204/EPTCS.176.1⟩
- Accès au texte intégral et bibtex
-
Book sections
- titre
- A Logical Basis for Quantum Evolution and Entanglement
- auteur
- Richard Blute, Alessio Guglielmi, Ivan T. Ivanov, Prakash Panangaden, Lutz Strassburger
- article
- Categories and Types in Logic, Language, and Physics – Essays Dedicated to Jim Lambek on the Occasion of His 90th Birthday, 8222, Springer, pp.90 – 107, 2014, ⟨10.1007/978-3-642-54789-8_6⟩
- Accès au texte intégral et bibtex
-
Habilitation à diriger des recherches
- titre
- Polarities & Focussing: a journey from Realisability to Automated Reasoning
- auteur
- Stéphane Graham-Lengrand
- article
- Logic in Computer Science [cs.LO]. Paris-Sud XI, 2014
- Accès au texte intégral et bibtex
-
Books
- titre
- Proceedings of the Joint Meeting of the Twenty-Third EACSL Annual Conference on Computer Science Logic (CSL) and the Twenty-Ninth Annual ACM/IEEE Symposium on Logic in Computer Science (LICS)
- auteur
- Thomas Henzinger, Dale Miller
- article
- ACM, pp.1-764, 2014, 978-1-4503-2886-9
- Accès au bibtex
-
- titre
- Special issue on computational logic in honour of Roy Dyckhoff. Journal of Logic and Computation.
- auteur
- Didier Galmiche, Stéphane Graham-Lengrand
- article
- Oxford University Press, 2014, D M Gabbay
- Accès au bibtex
-
Preprints, Working Papers, …
- titre
- An interpretation of the Sigma-2 fragment of classical Analysis in System T
- auteur
- Danko Ilik
- article
- 2014
- Accès au texte intégral et bibtex
-
- titre
- Structural Interactions and Absorption of Structural Rules in BI Sequent Calculus
- auteur
- Ryuta Arisaka
- article
- 2014
- Accès au texte intégral et bibtex
-
- titre
- Gradual Classical Logic for Attributed Objects
- auteur
- Ryuta Arisaka
- article
- 2014
- Accès au texte intégral et bibtex
-
2013
Journal articles
- titre
- A formal framework for specifying sequent calculus proof systems
- auteur
- Dale Miller, Elaine Pimentel
- article
- Theoretical Computer Science, 2013, pp.98-116. ⟨10.1016/j.tcs.2012.12.008⟩
- Accès au bibtex
-
- titre
- Kripke Semantics and Proof Systems for Combining Intuitionistic Logic and Classical Logic
- auteur
- Chuck Liang, Dale Miller
- article
- Annals of Pure and Applied Logic, 2013, 164 (2), pp.86-111. ⟨10.1016/j.apal.2012.09.005⟩
- Accès au texte intégral et bibtex
-
- titre
- Herbrand-Confluence
- auteur
- Stefan Hetzl, Lutz Strassburger
- article
- Logical Methods in Computer Science, 2013, 9 (4), pp.1-25. ⟨10.2168/LMCS-9(4:24)2013⟩
- Accès au bibtex
-
- titre
- Non-idempotent intersection types and strong normalisation
- auteur
- Alexis Bernadet, Stéphane Graham-Lengrand
- article
- Logical Methods in Computer Science, 2013, 9 (4), pp.17-42
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Reasoning About Higher-Order Relational Specifications
- auteur
- Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek, Gopalan Nadathur
- article
- International Symposium on Principles and Practice of Declarative Programming, ACM SIGPLAN, Sep 2013, Madrid, Spain. ⟨10.1145/2505879.2505889⟩
- Accès au texte intégral et bibtex
-
- titre
- Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture
- auteur
- Stéphane Graham-Lengrand
- article
- 22nd International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux’13), Sep 2013, Nancy, France. pp.149–156
- Accès au texte intégral et bibtex
-
- titre
- A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus
- auteur
- Mahfuza Farooque, Stéphane Lengrand, Assia Mahboubi
- article
- LFMTP – International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice – 2013, Sep 2013, Boston, United States. ⟨10.1145/2503887.2503892⟩
- Accès au texte intégral et bibtex
-
- titre
- Subformula Linking as an Interaction Method
- auteur
- Kaustuv Chaudhuri
- article
- 4th Conference on Interactive Theorem Proving, Jul 2013, Rennes, France. pp.386-401, ⟨10.1007/978-3-642-39634-2_28⟩
- Accès au texte intégral et bibtex
-
- titre
- Unifying Classical and Intuitionistic Logics for Computational Control
- auteur
- Chuck Liang, Dale Miller
- article
- LOGIC IN COMPUTER SCIENCE (LICS 2013), Jun 2013, New Orleans, United States
- Accès au texte intégral et bibtex
-
- titre
- Checking foundational proof certificates for first-order logic
- auteur
- Zakaria Chihani, Dale Miller, Fabien Renaud
- article
- PxTP – Proof Exchange for Theorem Proving, Jun 2013, Lake Placid, United States
- Accès au texte intégral et bibtex
-
- titre
- Foundational proof certificates in first-order logic
- auteur
- Zakaria Chihani, Dale Miller, Fabien Renaud
- article
- CADE – 24th International Conference on Automated Deduction, Jun 2013, Lake Placid, United States
- Accès au texte intégral et bibtex
-
- titre
- A Hybrid Linear Logic for Constrained Transition Systems
- auteur
- Joelle Despeyroux, Kaustuv Chaudhuri
- article
- TYPES 2013 – 19th International Conference on Types for Proofs and Programs, Apr 2013, Toulouse, France. pp.150-168
- Accès au texte intégral et bibtex
-
- titre
- Cut Elimination in Nested Sequents for Intuitionistic Modal Logics
- auteur
- Lutz Strassburger
- article
- FoSSaCS 2013, Mar 2013, Rome, Italy. pp.209-224, ⟨10.1007/978-3-642-37075-5_14⟩
- Accès au texte intégral et bibtex
-
- titre
- Preserving differential privacy under finite-precision semantics
- auteur
- Ivan Gazeau, Dale Miller, Catuscia Palamidessi
- article
- QAPL – 11th International Workshop on Quantitative Aspects of Programming Languages and Systems, Mar 2013, Rome, Italy. pp.1-18, ⟨10.4204/EPTCS.117.1⟩
- Accès au texte intégral et bibtex
-
Books
- titre
- Proceedings of the Sixth Workshop on Intersection Types and Related Systems (ITRS’12)
- auteur
- Stéphane Graham-Lengrand, Luca Paolini
- article
- EPTCS, 121, pp.1–93, 2013, ⟨10.4204/EPTCS.121⟩
- Accès au bibtex
-
Reports
- titre
- A Hybrid Linear Logic for Constrained Transition Systems with Applications to Molecular Biology
- auteur
- Kaustuv Chaudhuri, Joelle Despeyroux
- article
- [Research Report] 2013, pp.30
- Accès au texte intégral et bibtex
-
- titre
- Automated reasoning techniques as proof-search in sequent calculus
- auteur
- Mahfuza Farooque
- article
- 2013
- Accès au texte intégral et bibtex
-
- titre
- Sequent Calculi with procedure calls
- auteur
- Mahfuza Farooque, Stéphane Graham-Lengrand
- article
- 2013
- Accès au texte intégral et bibtex
-
Theses
- titre
- Automated Reasoning Techniques as Proof-search in Sequent Calculus
- auteur
- Mahfuza Farooque
- article
- Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2013. English. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
- titre
- Programmation sûre en précision finie : Contrôler les erreurs et les fuites d’informations
- auteur
- Ivan Gazeau
- article
- Analyse numérique [cs.NA]. Ecole Polytechnique X, 2013. Français. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
- titre
- Nested Deduction in Logical Foundations for Computation
- auteur
- Nicolas Guenot
- article
- Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2013. English. ⟨NNT : ⟩
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, …
- titre
- Path Functors in Cat
- auteur
- François Lamarche
- article
- 2013
- Accès au texte intégral et bibtex
-
- titre
- Extracting Proofs from Tabled Proof Search
- auteur
- Dale Miller, Alwen Tiu
- article
- 2013
- Accès au texte intégral et bibtex
-
- titre
- Communicating and trusting proofs: The case for foundational proof certificates
- auteur
- Dale Miller
- article
- 2013
- Accès au texte intégral et bibtex
-
2012
Journal articles
- titre
- A two-level logic approach to reasoning about computations
- auteur
- Andrew Gacek, Dale Miller, Gopalan Nadathur
- article
- Journal of Automated Reasoning, 2012, 49 (2), pp.241-273. ⟨10.1007/s10817-011-9218-1⟩
- Accès au bibtex
-
- titre
- Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus
- auteur
- Beniamino Accattoli, Delia Kesner
- article
- Logical Methods in Computer Science, 2012, 8 (1), pp.44. ⟨10.2168/LMCS-8(1:28)2012⟩
- Accès au bibtex
-
- titre
- Extension without Cut
- auteur
- Lutz Strassburger
- article
- Annals of Pure and Applied Logic, 2012, 163 (12), pp.1995-2007. ⟨10.1016/j.apal.2012.07.004⟩
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Proof pearl: abella formalization of lambda-calculus cube property
- auteur
- Beniamino Accattoli
- article
- Second international conference on Certified Programs and Proofs, Dec 2012, Kyoto, Japan
- Accès au texte intégral et bibtex
-
- titre
- Compact Proof Certificates for Linear Logic
- auteur
- Kaustuv Chaudhuri
- article
- Second International Conference on Certified Programs and Proofs, Dec 2012, Kyoto, Japan. pp.208–223, ⟨10.1007/978-3-642-35308-6_17⟩
- Accès au texte intégral et bibtex
-
- titre
- Proof-Nets and the Call-by-Value Lambda-Calculus
- auteur
- Beniamino Accattoli
- article
- Seventh Workshop on Logical and Semantic Frameworks, with Applications, Sep 2012, Rio de Janeiro, Brazil. ⟨10.4204/EPTCS.113.5⟩
- Accès au texte intégral et bibtex
-
- titre
- Herbrand-Confluence for Cut Elimination in Classical First Order Logic
- auteur
- Stefan Hetzl, Lutz Strassburger
- article
- CSL 2012, Sep 2012, Fontainebleau, France. ⟨10.4230/LIPIcs.CSL.2012.320⟩
- Accès au texte intégral et bibtex
-
- titre
- A Systematic Approach to Canonicity in the Classical Sequent Calculus
- auteur
- Kaustuv Chaudhuri, Stefan Hetzl, Dale Miller
- article
- 21st EACSL Annual Conference on Computer Science Logic, Sep 2012, Fontainebleau, France. pp.183-197, ⟨10.4230/LIPIcs.CSL.2012.183⟩
- Accès au texte intégral et bibtex
-
- titre
- Project Presentation: Algorithmic Structuring and Compression of Proofs (ASCOP)
- auteur
- Stefan Hetzl
- article
- Conferences on Intelligent Computer Mathematics (CICM) 2012, Jul 2012, Bremen, Germany
- Accès au texte intégral et bibtex
-
- titre
- On the Invariance of the Unitary Cost Model for Head Reduction
- auteur
- Beniamino Accattoli, Ugo Dal Lago
- article
- 23rd International Conference on Rewriting Techniques and Applications (RTA’12), May 2012, Nagoya, Japan
- Accès au texte intégral et bibtex
-
- titre
- An abstract factorization theorem for explicit substitutions
- auteur
- Beniamino Accattoli
- article
- 23rd International Conference on Rewriting Techniques and Applications (RTA’12), May 2012, Nagoya, Japan
- Accès au texte intégral et bibtex
-
- titre
- Call-by-Value solvability, revisited
- auteur
- Beniamino Accattoli, Luca Paolini
- article
- 11th International Symposium on Functional and Logic Programming – FLOPS 2012, May 2012, Kobe, Japan
- Accès au texte intégral et bibtex
-
- titre
- A non-local method for robustness analysis of floating point programs
- auteur
- Ivan Gazeau, Dale Miller, Catuscia Palamidessi
- article
- QAPL – Tenth Workshop on Quantitative Aspects of Programming Languages, Mar 2012, Tallinn, Estonia. pp.63-76, ⟨10.4204/EPTCS.85.5⟩
- Accès au texte intégral et bibtex
-
- titre
- The permutative lambda calculus
- auteur
- Beniamino Accattoli, Delia Kesner
- article
- 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning – LPAR-18, Mar 2012, Merida, Venezuela
- Accès au texte intégral et bibtex
-
Books
- titre
- Proceedings 8th Workshop on Fixed Points in Computer Science
- auteur
- Dale Miller, Zoltán Ésik
- article
- Electronic Proceedings in Theoretical Computer Science, 77, pp.61, 2012, ⟨10.4204/EPTCS.77⟩
- Accès au bibtex
-
- titre
- Automated Reasoning: 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 2012, Proceedings
- auteur
- Gramlich Bernhard, Dale Miller, Sattler Uli
- article
- Springer, 7364, pp.1-568, 2012, Lecture Notes in Artificial Intelligence, ⟨10.1007/978-3-642-31365-3⟩
- Accès au bibtex
-
- titre
- CPP 2012: Second International Conference on Certified Programs and Proofs
- auteur
- Hawblitzel Chris, Dale Miller
- article
- Springer, 7679, pp.1-305, 2012, lncs, ⟨10.1007/978-3-642-35308-6⟩
- Accès au bibtex
-
- titre
- Programming with Higher-Order Logic
- auteur
- Dale Miller, Nadathur Gopalan
- article
- Cambridge University Press, pp.320, 2012, 9780521879408. ⟨10.1017/CBO9781139021326⟩
- Accès au bibtex
-
Reports
- titre
- A sequent calculus with procedure calls
- auteur
- Mahfuza Farooque, Stéphane Lengrand
- article
- 2012
- Accès au texte intégral et bibtex
-
- titre
- A simple presentation of the effective topos
- auteur
- Alexis Bernadet, Stéphane Graham-Lengrand
- article
- [Research Report] LIX, Ecole polytechnique. 2012
- Accès au texte intégral et bibtex
-
- titre
- Two simulations about DPLL(T)
- auteur
- Mahfuza Farooque, Stéphane Lengrand, Assia Mahboubi
- article
- 2012
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, …
- titre
- Simulating the DPLL(T ) procedure in a sequent calculus with focusing
- auteur
- Mahfuza Farooque, Stéphane Lengrand, Assia Mahboubi
- article
- 2012
- Accès au texte intégral et bibtex
-
2011
Journal articles
- titre
- A System of Interaction and Structure IV: The Exponentials and Decomposition
- auteur
- Lutz Strassburger, Alessio Guglielmi
- article
- ACM Transactions on Computational Logic, 2011, 12 (4), pp.23. ⟨10.1145/1970398.1970399⟩
- Accès au texte intégral et bibtex
-
- titre
- A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems
- auteur
- Stéphane Lengrand, Roy Dyckhoff, James Mckinna
- article
- Logical Methods in Computer Science, 2011, 7 (1), pp.33. ⟨10.2168/LMCS-7(1:6)2011⟩
- Accès au texte intégral et bibtex
-
- titre
- A System of Interaction and Structure V: The Exponentials and Splitting
- auteur
- Alessio Guglielmi, Lutz Strassburger
- article
- Mathematical Structures in Computer Science, 2011, pp.1-22. ⟨10.1017/S096012951100003X⟩
- Accès au texte intégral et bibtex
-
- titre
- Nominal Abstraction
- auteur
- Gacek Andrew, Dale Miller, Gopalan Nadathur
- article
- Information and Computation, 2011, 209 (1), pp.48-73
- Accès au texte intégral et bibtex
-
- titre
- From Deep Inference to Proof Nets via Cut Elimination
- auteur
- Lutz Strassburger
- article
- Journal of Logic and Computation, 2011, 21 (4), pp.589-624. ⟨10.1093/logcom/exp047⟩
- Accès au bibtex
-
- titre
- A Focused Approach to Combining Logics
- auteur
- Chuck Liang, Dale Miller
- article
- Annals of Pure and Applied Logic, 2011, ⟨10.1016/j.apal.2011.01.012⟩
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Complexity of strongly normalising λ-terms via non-idempotent intersection types
- auteur
- Alexis Bernadet, Stéphane Lengrand
- article
- Proceedings of the 14th International Conference on Foundations of Software Science and Computation Structures (FOSSACS’11), Sep 2011, Saarbruecken, Germany. pp.88-107, ⟨10.1007/978-3-642-19805-2_7⟩
- Accès au bibtex
-
- titre
- Filter models: non-idempotent intersection types, orthogonality and polymorphism
- auteur
- Alexis Bernadet, Stéphane Lengrand
- article
- Proceedings of the 20th Annual Conference of the European Association for Computer Science Logic (CSL’11), Sep 2011, Bergen, Norway. ⟨10.4230/LIPIcs.CSL.2011.51⟩
- Accès au bibtex
-
- titre
- The Focused Calculus of Structures
- auteur
- Kaustuv Chaudhuri, Nicolas Guenot, Lutz Strassburger
- article
- 20th EACSL Annual Conference on Computer Science Logic, Sep 2011, Bergen, Norway. pp.159-173, ⟨10.4230/LIPIcs.CSL.2011.159⟩
- Accès au texte intégral et bibtex
-
- titre
- A proposal for broad spectrum proof certificates
- auteur
- Dale Miller
- article
- CPP 2011 – First International Conference on Certified Proofs and Programs, 2011, Kenting, Taiwan
- Accès au texte intégral et bibtex
-
Habilitation à diriger des recherches
- titre
- Towards a Theory of Proofs of Classical Logic
- auteur
- Lutz Strassburger
- article
- Logic in Computer Science [cs.LO]. Université Paris-Diderot – Paris VII, 2011
- Accès au texte intégral et bibtex
-
Preprints, Working Papers, …
- titre
- Orthogonality and Boolean Algebras for Deduction Modulo
- auteur
- Alois Brunel, Olivier Hermant, Clement Houtmann
- article
- 2011
- Accès au texte intégral et bibtex
-
2010
Journal articles
- titre
- A framework for proof systems
- auteur
- Nigam Vivek, Dale Miller
- article
- Journal of Automated Reasoning, 2010, 45 (2)
- Accès au texte intégral et bibtex
-
- titre
- Proof and Refutation in MALL as a game
- auteur
- Olivier Delande, Dale Miller, Alexis Saurin
- article
- Annals of Pure and Applied Logic, 2010, 161 (5), pp.654-672. ⟨10.1016/j.apal.2009.07.017⟩
- Accès au bibtex
-
- titre
- Proof Search Specifications of the pi-calculus
- auteur
- Tiu Alwen, Dale Miller
- article
- ACM Transactions on Computational Logic, 2010, 11 (2)
- Accès au texte intégral et bibtex
-
Conference papers
- titre
- Magically Constraining the Inverse Method Using Dynamic Polarity Assignment
- auteur
- Kaustuv Chaudhuri
- article
- Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), Oct 2010, Yogyakarta, Indonesia. pp.202–216, ⟨10.1007/978-3-642-16242-8_15⟩
- Accès au texte intégral et bibtex
-
- titre
- The TLA+ Proof System: Building a Heterogeneous Verification Platform
- auteur
- Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
- article
- International Conference on Theoretical Aspects of Computing – ICTAC 2010, Sep 2010, Natal, Brazil. pp.44, ⟨10.1007/978-3-642-14808-8_3⟩
- Accès au bibtex
-
- titre
- Classical and Intuitionistic Subexponential Logics are Equally Expressive
- auteur
- Kaustuv Chaudhuri
- article
- Computer Science Logic, Aug 2010, Brno, Czech Republic. pp.185–199, ⟨10.1007/978-3-642-15205-4_17⟩
- Accès au texte intégral et bibtex
-
- titre
- Verifying Safety Properties With the TLA+ Proof System
- auteur
- Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, Stephan Merz
- article
- Fifth International Joint Conference on Automated Reasoning – IJCAR 2010, Jul 2010, Edinburgh, United Kingdom. pp.142–148, ⟨10.1007/978-3-642-14203-1_12⟩
- Accès au texte intégral et bibtex
-
- titre
- Focused Inductive Theorem Proving
- auteur
- David Baelde, Dale Miller, Zachary Snow
- article
- IJCAR 2010 – International Joint Conference on Automated Deduction, 2010, Edinburgh, United Kingdom
- Accès au texte intégral et bibtex
-
- titre
- Reasoning about computations using two-levels of logic
- auteur
- Dale Miller
- article
- APLAS 2010: Eighth Asian Symposium on Programming Languages and Systems, 2010, Shanghai, China
- Accès au texte intégral et bibtex
-
- titre
- Finding Unity in Computational Logic
- auteur
- Dale Miller
- article
- ACM-BCS Visions of Computer Science, 2010, Edinburgh, United Kingdom
- Accès au texte intégral et bibtex
-
2009
Journal articles
- titre
- Focusing and Polarization in Linear, Intuitionistic, and Classical Logics
- auteur
- Chuck Liang, Dale Miller
- article
- Theoretical Computer Science, 2009, 410 (46), ⟨10.1016/j.tcs.2009.07.041⟩
- Accès au bibtex
-
Conference papers
- titre
- Algorithmic specifications in linear logic with subexponentials
- auteur
- Nigam Vivek, Dale Miller
- article
- PPDP09 – ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, Sep 2009, Coimbra, Portugal
- Accès au bibtex
-
- titre
- A Unified Sequent Calculus for Focused Proofs
- auteur
- Liang Chuck, Dale Miller
- article
- LICS 2009 – Twenty-Fourth Annual IEEE Symposium on LOGIC IN COMPUTER SCIENCE, Aug 2009, Los Angeles, United States
- Accès au bibtex
-
- titre
- Expanding the Realm of Systematic Proof Theory
- auteur
- Agata Ciabattoni, Lutz Strassburger, Kazushige Terui
- article
- Computer Science Logic, CSL’09, 2009, Coimbra, Portugal. ⟨10.1007/978-3-642-04027-6_14⟩
- Accès au texte intégral et bibtex
-
- titre
- A Kleene Theorem for Forest Languages
- auteur
- Lutz Strassburger
- article
- Language and Automata Theory and Applications, LATA’09, 2009, Tarragona, Spain
- Accès au bibtex
-
- titre
- Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic
- auteur
- Lutz Strassburger
- article
- Typed Lambda Calculi and Applications, TLCA’09, 2009, Brasilia, Brazil. ⟨10.1007/978-3-642-02273-9_23⟩
- Accès au bibtex
-
- titre
- Modular Sequent Systems for Modal Logic
- auteur
- Kai Brünnler, Lutz Strassburger
- article
- Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX’09, 2009, Oslo, Norway
- Accès au bibtex
-
2008
Conference papers
- titre
- Towards Ludics Programming: Interactive Proof Search
- auteur
- Alexis Saurin
- article
- 24th International Conference on Logic Programming – ICLP 2008, Dec 2008, Udine, Italy. pp.253-268, ⟨10.1007/978-3-540-89982-2_27⟩
- Accès au bibtex
-
- titre
- On the Relations between the Syntactic Theories of $\lambda\mu$-Calculi
- auteur
- Alexis Saurin
- article
- 17th EACSL Annual Conference on Computer Science Logic – CSL 2008, Sep 2008, Bertinoro, Italy. pp.154-168, ⟨10.1007/978-3-540-87531-4_13⟩
- Accès au bibtex
-
- titre
- Canonical Sequent Proofs via Multi-Focusing
- auteur
- Alexis Saurin, Kaustuv C. Chaudhuri, Dale Miller
- article
- Fifth IFIP International Conference On Theoretical Computer Science – TCS 2008, IFIP 20th World Computer Congress, Sep 2008, Milano, Italy. pp.383-396, ⟨10.1007/978-0-387-09680-3_26⟩
- Accès au bibtex
-
Reports
- titre
- Stream Associative Nets and Lambda-mu-calculus
- auteur
- Michele Pagani, Alexis Saurin
- article
- [Research Report] RR-6431, INRIA. 2008, pp.48
- Accès au texte intégral et bibtex
-
2007
Conference papers
- titre
- Focusing and Polarization in Intuitionistic Logic
- auteur
- Chuck Liang, Dale Miller
- article
- Computer Science Logic, Sep 2007, Lausanne, Switzerland
- Accès au texte intégral et bibtex
-
- titre
- From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic
- auteur
- Alexis Saurin, Dale Miller
- article
- 16th EACSL Annual Conference on Computer Science and Logic – CSL 2007, Sep 2007, Lausanne, Switzerland. pp.405-419, ⟨10.1007/978-3-540-74915-8_31⟩
- Accès au bibtex
-
- titre
- Deep Inference for Hybrid Logic
- auteur
- Lutz Strassburger
- article
- International Workshop on Hybrid Logic 2007 (HyLo 2007), Aug 2007, Dublin, Ireland
- Accès au texte intégral et bibtex
-
- titre
- A Characterisation of Medial as Rewriting Rule
- auteur
- Lutz Strassburger
- article
- RTA 2007, Jun 2007, Paris, France
- Accès au texte intégral et bibtex
-
2006
Conference papers
- titre
- What could a Boolean category be?
- auteur
- Lutz Strassburger
- article
- Classical Logic and Computation 2006 (ICALP Workshop), Jul 2006, Venice, Italy
- Accès au texte intégral et bibtex
-
- titre
- Collection analysis for Horn clause programs
- auteur
- Dale Miller
- article
- International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, Jul 2006, Venice, Italy
- Accès au texte intégral et bibtex
-
Other publications
- titre
- On the Axiomatisation of Boolean Categories with and without Medial
- auteur
- Lutz Strassburger
- article
- 2006
- Accès au texte intégral et bibtex
-
Reports
- titre
- Proof Nets and the Identity of Proofs
- auteur
- Lutz Strassburger
- article
- [Research Report] RR-6013, INRIA. 2006
- Accès au texte intégral et bibtex
-
2005
Conference papers
- titre
- A Congruence Format for Name-passing Calculi
- auteur
- Axelle Ziegler, Dale Miller, Catuscia Palamidessi
- article
- 2nd Workshop on Structural Operational Semantics (SOS’05), Jul 2005, Lisboa, Portugal. pp.169-189, ⟨10.1016/j.entcs.2005.09.032⟩
- Accès au texte intégral et bibtex
-
- titre
- From Deep Inference to Proof Nets
- auteur
- Lutz Strassburger
- article
- Structures and Deduction 2005 (ICALP Workshop), Jul 2005, Lisbon, Portugal
- Accès au texte intégral et bibtex
-
- titre
- Separation with streams in the $\Lambda\mu$-calculus
- auteur
- Alexis Saurin
- article
- 20th Annual IEEE Symposium on Logic In Computer Science – LICS 2005, Jun 2005, Chicago, United States. pp.356-365, ⟨10.1109/LICS.2005.48⟩
- Accès au bibtex
-
- titre
- A game semantics for proof search, preliminary results
- auteur
- Alexis Saurin, Dale Miller
- article
- Twenty-first Conference on the Mathematical Foundations of Programming Semantics – MFPS XXI, May 2005, Birmingham, United Kingdom. pp.543-563, ⟨10.1016/j.entcs.2005.11.072⟩
- Accès au bibtex
-
- titre
- Constructing free Boolean categories
- auteur
- François Lamarche, Lutz Strassburger
- article
- 20th Annual IEEE Symposium on Logic in Computer Science – LICS 2005, May 2005, Chicago/USA, United States. pp.209- 218, ⟨10.1109/LICS.2005.13⟩
- Accès au texte intégral et bibtex
-
Book sections
- titre
- What is a logic, and what is a proof ?
- auteur
- Lutz Strassburger
- article
- Jean-Yves Beziau. Logica Universalis, Birkhäuser, pp.135-145, 2005, 978-3-7643-7259-0
- Accès au texte intégral et bibtex
-
