Publications available via HAL

Publications HAL du labo/EPI parsifal

2019

Journal articles

titre
An Intuitionistic Formula Hierarchy Based on High-School Identities
auteur
Taus Brock-Nannestad, Danko Ilik
article
Mathematical Logic Quarterly, Wiley, 2019, 65 (1), pp.57-79. ⟨10.1002/malq.201700047⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01354181/file/high-school.pdf BibTex
titre
Hybrid Linear Logic, revisited
auteur
Kaustuv Chaudhuri, Carlos Olarte, Elaine Pimentel, Joëlle Despeyroux
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), In press
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01968154/file/MSCS_HAL.pdf BibTex

Conference papers

titre
Un mécanisme de preuve par réflexion pour Why3 et son application aux algorithmes de GMP
auteur
Simon Colin, Rodolphe Lepigre, Gabriel Scherer
article
JFLA 2019 – 30 èmes journ ́ees francophones des langages applicatifs, Jan 2019, Les Rousses, France
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01929508/file/1811.02300.pdf BibTex

2018

Journal articles

titre
Deep inference and expansion trees for second-order multiplicative linear logic
auteur
Lutz Straßburger
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2018, pp.1-31. ⟨10.1017/S0960129518000385⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01942410/file/ExpTreesLL.pdf 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, ACM, 2018, 2 (ICFP), pp.1 – 15. ⟨10.1145/3236798⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01929161/file/1807.06702.pdf BibTex
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, ACM, 2018, 2 (ICFP), pp.1 – 29. ⟨10.1145/3236771⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01929178/file/1710.10385.pdf BibTex
titre
Maehara-style modal nested calculi
auteur
Roman Kuznets, Lutz Straßburger
article
Archive for Mathematical Logic, Springer Verlag, 2018, ⟨10.1007/s00153-018-0636-1⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01942240/file/10.1007%252Fs00153-018-0636-1.pdf BibTex
titre
Proof Diagrams for Multiplicative Linear Logic: Syntax and Semantics
auteur
Matteo Acclavio
article
Journal of Automated Reasoning, Springer Verlag, 2018, ⟨10.1007/s10817-018-9466-4⟩
Accès au bibtex
BibTex
titre
Mechanized metatheory revisited
auteur
Dale Miller
article
Journal of Automated Reasoning, Springer Verlag, In press
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01884210/file/paper.pdf BibTex
titre
A proof theory for model checking
auteur
Quentin Heath, Dale Miller
article
Journal of Automated Reasoning, Springer Verlag, In press, ⟨10.1007/s10817-018-9475-3⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01814006/file/hal.pdf 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, ACM, 2018, 2 (POPL), ⟨https://popl18.sigplan.org/⟩. ⟨10.1145/3158137⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01646765/file/sourir.pdf BibTex
titre
Expressing Additives Using Multiplicatives and Subexponentials
auteur
Kaustuv Chaudhuri
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2018, 28 (5), pp.651-666
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01222767/file/main.pdf BibTex

Conference papers

titre
Types of Fireballs
auteur
Beniamino Accattoli, Giulio Guerrieri
article
16th Asian Symposium on Programming Languages and System (APLAS 2018), Dec 2018, Wellington, New Zealand
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01967531/file/Accattoli%2C%20Guerrieri%20-%20Types%20of%20Fireballs.pdf 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
https://hal.archives-ouvertes.fr/hal-01967532/file/Accattoli%20-%20Proof%20Nets%20and%20the%20Linear%20Substitution%20Calcuuls.pdf 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
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
https://hal.archives-ouvertes.fr/hal-01936141/file/main.pdf 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
https://hal.inria.fr/hal-01806154/file/paper.pdf 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
https://hal.inria.fr/hal-01870112/file/admissible.pdf 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
https://hal.inria.fr/hal-01806129/file/paper%20%281%29.pdf 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
https://hal.archives-ouvertes.fr/hal-01935591/file/BobotEtAl-SMT2018.pdf 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
https://hal.inria.fr/hal-01929158/file/1707.04984.pdf 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
https://hal.archives-ouvertes.fr/hal-01935578/file/paper.pdf 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
https://hal.inria.fr/hal-01682691/file/jfla2018.pdf 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
https://hal.inria.fr/hal-01968139/file/simsub_hal.pdf 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
https://hal.archives-ouvertes.fr/hal-01935595/file/CDSATproofs.pdf BibTex

Book sections

titre
From Syntactic Proofs to Combinatorial Proofs
auteur
Matteo Acclavio, Lutz Straßburger
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
https://hal.inria.fr/hal-01942275/file/tableau-def.pdf 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
https://hal.inria.fr/hal-01900891/file/hapop2018.pdf BibTex

Reports

titre
On the Decision Problem for MELL
auteur
Lutz Straßburger
article
[Research Report] 9203, Inria Saclay Ile de France. 2018
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01870148/file/RR-9203.pdf BibTex
titre
Proof nets for first-order additive linear logic
auteur
Willem Heijltjes, Dominic Hughes, Lutz Straßburger
article
[Research Report] RR-9201, Inria. 2018
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01867625/file/RR-9201.pdf 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), College Publications, 2017, 4 (10), pp.3487-3508
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01354180/file/KGS-book-chapter-danko.pdf BibTex
titre
On the Value of Variables
auteur
Beniamino Accattoli, Claudio Sacerdoti Coen
article
Information and Computation, Elsevier, 2017, 255, pp.224 – 242. ⟨10.1016/j.ic.2017.01.003⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01675373/file/main.pdf BibTex
titre
A Semantic Framework for Proof Evidence
auteur
Zakaria Chihani, Dale Miller, Fabien Renaud
article
Journal of Automated Reasoning, Springer Verlag, 2017, 59 (3), pp.287-330. ⟨10.1007/s10817-016-9380-6⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01390912/file/fpc-jar.pdf BibTex
titre
Proof Checking and Logic Programming
auteur
Dale Miller
article
Formal Aspects of Computing, Springer Verlag, 2017, 29 (3), pp.383-399 ⟨10.1007/s00165-016-0393-z⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01390901/file/paper.pdf 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
https://hal.archives-ouvertes.fr/hal-01675369/file/Accattoli%2C%20Barras%20-%20The%20Negligible%20and%20Yet%20Subtle%20Cost%20of%20Pattern%20Matching.pdf 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
https://hal.archives-ouvertes.fr/hal-01675358/file/p4-accattoli.pdf BibTex
titre
Proof theory for indexed nested sequents
auteur
Sonia Marin, Lutz Straßburger
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
https://hal.inria.fr/hal-01635935/file/Tableaux17.pdf 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
https://hal.inria.fr/hal-01646788/file/lfmtp17.pdf 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
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
https://hal.archives-ouvertes.fr/hal-01615673/file/tlla2017.pdf BibTex
titre
Combinatorial Flows and their Normalisation
auteur
Lutz Straßburger
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
https://hal.inria.fr/hal-01635931/file/comproofcom-finalforFSCD17.pdf 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
https://hal.inria.fr/hal-01615683/file/CSL_2017_paper_66.pdf BibTex
titre
Satisfiability Modulo Theories and Assignments
auteur
Maria 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
https://hal.archives-ouvertes.fr/hal-01615830/file/CDSATpaper.pdf 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
https://hal.inria.fr/hal-01645016/file/cade2017.pdf 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
https://hal.archives-ouvertes.fr/hal-01615837/file/SMT2017.pdf BibTex
titre
On the Length of Medial-Switch-Mix Derivations
auteur
Paola Bruscoli, Lutz Straßburger
article
WoLLIC 2017 – Logic, Language, Information, and Computation, Jul 2017, London, United Kingdom
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01635933/file/sm-length.pdf 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
https://hal.archives-ouvertes.fr/hal-01675365/file/Accattoli%2C%20Guerrieri%20-%20Implementing%20Open%20CbV.pdf 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
https://hal.inria.fr/hal-01167162/file/explog.pdf BibTex
titre
Deciding equivalence with sums and the empty type
auteur
Gabriel Scherer
article
POPL 2017, Jan 2017, Paris, France. ⟨10.01213⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01646064/file/finite-sums.pdf 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
https://hal.archives-ouvertes.fr/hal-01419473/file/typeful-continuations.pdf 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
https://hal.inria.fr/hal-01615681/file/mmr-types.pdf BibTex

Directions of work or 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
BibTex

Documents associated with scientific events

titre
Justification logic for constructive modal logic *
auteur
Roman Kuznets, Sonia Marin, Lutz Straßburger
article
IMLA 2017 – 7th Workshop on Intuitionistic Modal Logic and Applications, Jul 2017, Toulouse, France. 2017, ⟨https://sites.google.com/site/modallogicimla2017/home⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01614707/file/main-IMLAversion.pdf BibTex

Reports

titre
Maehara-style Modal Nested Calculi
auteur
Lutz Straßburger, Roman Kuznets
article
[Research Report] RR-9123, Inria Saclay. 2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01644750/file/RR-9123.pdf BibTex
titre
Deep Inference, Expansion Trees, and Proof Graphs for Second Order Propositional Multiplicative Linear Logic
auteur
Lutz Straßburger
article
[Research Report] RR-9071, Inria Saclay Ile de France. 2017, pp.38
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01526831/file/RR-9071.pdf BibTex
titre
On the Proof Theory of Indexed Nested Sequents for Classical and Intuitionistic Modal Logics
auteur
Sonia Marin, Lutz Straßburger
article
[Research Report] RR-9061, Inria. 2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01515797/file/RR-9061.pdf BibTex
titre
Combinatorial Flows and Proof Compression
auteur
Lutz Straßburger
article
[Research Report] RR-9048, Inria Saclay. 2017
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01498468/file/RR-9048.pdf BibTex

Preprints, Working Papers, …

titre
Connected chord diagrams and bridgeless maps
auteur
Julien Courtiel, Karen Yeats, Noam Zeilberger
article
2017
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01650141/file/CoYeZe.pdf BibTex

2016

Journal articles

titre
On linear rewriting systems for Boolean logic and some applications to proof theory
auteur
Anupam Das, Lutz Straßburger
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2016
Accès au bibtex
https://arxiv.org/pdf/1610.08772 BibTex
titre
Linear lambda terms as invariants of rooted trivalent maps
auteur
Noam Zeilberger
article
Journal of Functional Programming, Cambridge University Press (CUP), 2016, 26, ⟨10.1017/S095679681600023X⟩
Accès au bibtex
https://arxiv.org/pdf/1512.06751 BibTex
titre
Proof nets and semi-star-autonomous categories
auteur
Willem Heijltjes, Lutz Straßburger
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2016, 26 (5), pp.789-828. ⟨10.1017/S0960129514000395⟩
Accès au bibtex
BibTex
titre
(Leftmost-outermost) beta reduction is invariant, indeed
auteur
Beniamino Accattoli, Ugo Dal Lago
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2016, ⟨10.2168/LMCS-12(1:4)2016⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01337712/file/lmcs2016.pdf BibTex
titre
Preserving differential privacy under finite-precision semantics
auteur
Ivan Gazeau, Dale Miller, Catuscia Palamidessi
article
Theoretical Computer Science, Elsevier, 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01390927/file/gazeau-draft-2014.pdf BibTex
titre
Proof Certificates for Equality Reasoning
auteur
Zakaria Chihani, Dale Miller
article
Electronic Notes in Theoretical Computer Science, Elsevier, 2016, 323, pp.93 – 108. ⟨10.1016/j.entcs.2016.06.007⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01390919/file/lsfa2015.pdf BibTex

Conference papers

titre
Non-crossing Tree Realizations of Ordered Degree Sequences
auteur
Laurent Mehats, Lutz Straßburger
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
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
https://hal.inria.fr/hal-01425465/file/Accattoli%2CGuerrieri-OpenCBV.pdf 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
https://hal.archives-ouvertes.fr/hal-01379625/file/LibVol-GandALF16.pdf 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
https://hal.archives-ouvertes.fr/hal-01379624/file/aiml2016.pdf 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
https://hal.inria.fr/hal-01425534/file/main.pdf 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
https://hal.archives-ouvertes.fr/hal-01424749/file/paper.pdf 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
https://hal.inria.fr/hal-01425560/file/Accattoli%20-%20The%20Complexity%20of%20Abstract%20Machines.pdf 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
https://hal.inria.fr/hal-01379683/file/fscd16.pdf BibTex
titre
Modular Focused Proof Systems for Intuitionistic Modal Logics
auteur
Kaustuv Chaudhuri, Sonia Marin, Lutz Straßburger
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
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
https://arxiv.org/pdf/1601.06098 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
https://hal.inria.fr/hal-01322335/file/final.pdf BibTex
titre
Focused and Synthetic Nested Sequents
auteur
Kaustuv Chaudhuri, Sonia Marin, Lutz Straßburger
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
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
https://hal.inria.fr/hal-01426753/file/flops16acyclicity.pdf 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
BibTex
titre
Focused and Synthetic Nested Sequents (Extended Technical Report)
auteur
Kaustuv Chaudhuri, Sonia Marin, Lutz Straßburger
article
[Research Report] Inria. 2016
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01251722/file/focused-nested.pdf 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
https://hal.inria.fr/hal-01422829/file/blanco-chihani.pdf 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
https://hal.inria.fr/hal-01354298/file/main.pdf BibTex

2015

Journal articles

titre
On Nested Sequents for Constructive Modal Logics
auteur
Ryuta Arisaka, Anupam Das, Lutz Straßburger
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2015, 11 (3), pp.1-33. ⟨10.2168/LMCS-11(3:7)2015⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01093143/file/1505.06896.pdf BibTex
titre
On the Power of Substitution in the Calculus of Structures
auteur
Lutz Straßburger, Novak Novakovic
article
ACM Transactions on Computational Logic, Association for Computing Machinery, 2015, 16 (3), ⟨http://dl.acm.org/citation.cfm?id=2701424⟩. ⟨10.1145/2701424⟩
Accès au bibtex
BibTex
titre
Proof nets and the call-by-value λ-calculus
auteur
Beniamino Accattoli
article
Theoretical Computer Science, Elsevier, 2015, ⟨10.1016/j.tcs.2015.08.006⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01244842/file/Accattoli%20-%20proof%20nets%20and%20the%20call-by-value%20lambda%20calculus%20%28long%20version%29.pdf 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
https://hal.archives-ouvertes.fr/hal-01244838/file/Accattoli%2C%20Barenbaum%2C%20Mazza%20-%20A%20Strong%20Distillery.pdf 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
https://hal.inria.fr/hal-01213858/file/MilVolLPAR15.pdf 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
https://hal.inria.fr/hal-01208362/file/lpar2015.pdf 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
https://hal.inria.fr/hal-01239753/file/subdelimlncs.pdf 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
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
https://hal.inria.fr/hal-01238434/file/iwil2015_paper.pdf 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
https://hal.inria.fr/hal-01238436/file/wof.pdf 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
https://hal.inria.fr/hal-01208333/file/tableaux2015.pdf 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
https://arxiv.org/pdf/1412.6790 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
https://hal.inria.fr/hal-01222592/file/disproving.pdf 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
https://hal.inria.fr/hal-01240172/file/pxtp2015.pdf 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
https://hal.inria.fr/hal-01208325/file/1507.08715v1.pdf 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
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
https://hal.inria.fr/hal-01211209/file/Main.pdf 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
https://hal.inria.fr/hal-01249216/file/ppdp15computation.pdf 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
https://hal.inria.fr/hal-01208346/file/complexity.pdf 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
https://hal.archives-ouvertes.fr/hal-01244833/file/Accattoli%2CSacerdotiCoen-OntheUsefulnessofFireballs.pdf 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
https://hal.inria.fr/hal-01222743/file/p00-wang.pdf BibTex
titre
No complete linear term rewriting system for propositional logic
auteur
Anupam Das, Lutz Straßburger
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
https://hal.inria.fr/hal-01236948/file/13.pdf 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
https://hal.inria.fr/hal-01242233/file/paper.pdf 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
https://hal.inria.fr/hal-01249220/file/mfps15fll-lambda.pdf 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
https://hal.inria.fr/hal-01091524/file/cpp-hal.pdf 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
BibTex

Directions of work or proceedings

titre
Proceedings Tenth International Workshop on Logical Frameworks and Meta Languages: Theory and Practice
auteur
Iliano Cervesato, Kaustuv Chaudhuri
article
Iliano Cervesato; Kaustuv Chaudhuri. Aug 2015, Berlin, Germany. 2015, ⟨10.4204/EPTCS.185⟩. ⟨http://lfmtp.org/workshops/2015⟩
Accès au bibtex
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
https://hal.inria.fr/hal-01222774/file/slides.pdf 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
https://hal.archives-ouvertes.fr/hal-01245442/file/spim-HAL-version.pdf 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
https://hal.archives-ouvertes.fr/hal-01213511/file/quantum-journal-preprint.pdf 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 , Leibniz-Zentrum für Informatik, 2014, pp.288-201. ⟨10.4230/LIPIcs.TYPES.2013.188⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01092427/file/11.pdf BibTex
titre
Proof nets and semi-star-autonomous categories
auteur
Willem Heijltjes, Lutz Straßburger
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2014, pp.1-40. ⟨http://journals.cambridge.org/action/displayAbstract?fromPage=online&aid=9408277&fileId=S0960129514000395⟩. ⟨10.1017/S0960129514000395⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01092253/file/fssac-final.pdf 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, American Medical Association (imprimé) / 2014, pp.306-14
Accès au bibtex
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, SAGE Publications, 2014, 20 (2), pp.234-42
Accès au bibtex
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, ASDD-AlmaDL, 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
https://hal.inria.fr/hal-01102709/file/abella-tutorial.pdf BibTex
titre
Modeling Martin Löf Type Theory in Categories
auteur
François Lamarche
article
Journal of Applied Logic, Elsevier, 2014, 12 (1), pp.28-44. ⟨10.1016/j.jal.2013.08.003⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00706562/file/IdentityTypesElsev.pdf BibTex
titre
A Multi-Focused Proof System Isomorphic to Expansion Proofs
auteur
Kaustuv Chaudhuri, Stefan Hetzl, Dale Miller
article
Journal of Logic and Computation, Oxford University Press (OUP), 2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00937056/file/lkfexp.pdf 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
https://hal.inria.fr/hal-01091544/file/abella-lf-hal.pdf BibTex
titre
Parametricity and Proving Free Theorems for Functional-Logic Languages
auteur
Stefan Mehner, Daniel Seidel, Lutz Straßburger, 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
https://hal.inria.fr/hal-01092357/file/ppdp2014-final.pdf BibTex
titre
Label-free Modular Systems for Classical and Intuitionistic Modal Logics
auteur
Sonia Marin, Lutz Straßburger
article
Advances in Modal Logic 10, Aug 2014, Groningen, Netherlands
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01092148/file/modul-modal.pdf 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
https://hal.inria.fr/hal-01091555/file/lfmtp14-hal.pdf 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
https://hal.inria.fr/hal-01096154/file/WeakMonProofsPHP-Extended.pdf 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
https://hal.inria.fr/hal-01091570/file/eqfix-hal.pdf 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
https://hal.inria.fr/hal-00991147/file/sumaxioms.pdf BibTex
titre
Symmetric Normalisation for Intuitionistic Logic
auteur
Nicolas Guenot, Lutz Straßburger
article
CSL-LICS 2014, Jul 2014, Vienna, Austria. ⟨10.1145/2603088.2603160⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-01092105/file/sjs2-final-with-appendix.pdf 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
https://hal.inria.fr/hal-00998753/file/main.pdf BibTex

Book sections

titre
A Logical Basis for Quantum Evolution and Entanglement
auteur
Richard Blute, Alessio Guglielmi, Ivan T. Ivanov, Prakash Panangaden, Lutz Straßburger
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
https://hal.inria.fr/hal-01092279/file/BVquantanewer-finalLNCS.pdf BibTex

Directions of work or proceedings

titre
Special issue on computational logic in honour of Roy Dyckhoff. Journal of Logic and Computation.
auteur
Didier Galmiche, Stéphane Graham-Lengrand
article
United Kingdom. Oxford University Press, 2014, ⟨http://dx.doi.org/10.1093/logcom/exu039⟩
Accès au bibtex
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
https://tel.archives-ouvertes.fr/tel-01094980/file/Main.pdf 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. ⟨http://dl.acm.org/citation.cfm?id=2603088⟩
Accès au bibtex
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
https://hal.inria.fr/hal-01092411/file/shift-analysis.pdf 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
https://hal.inria.fr/hal-00982331/file/workA.pdf BibTex
titre
Gradual Classical Logic for Attributed Objects
auteur
Ryuta Arisaka
article
2014
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00969271/file/aiPaper.pdf BibTex

2013

Journal articles

titre
A formal framework for specifying sequent calculus proof systems
auteur
Dale Miller, Elaine Pimentel
article
Theoretical Computer Science, Elsevier, 2013, pp.98-116. ⟨10.1016/j.tcs.2012.12.008⟩
Accès au bibtex
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, Elsevier Masson, 2013, 164 (2), pp.86-111. ⟨10.1016/j.apal.2012.09.005⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00787601/file/pil-final.pdf BibTex
titre
Non-idempotent intersection types and strong normalisation
auteur
Alexis Bernadet, Stéphane Graham-Lengrand
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2013, 9 (4), pp.17-42
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00906778/file/Journal13.pdf BibTex
titre
Herbrand-Confluence
auteur
Stefan Hetzl, Lutz Straßburger
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2013, 9 (4), pp.1-25. ⟨10.2168/LMCS-9(4:24)2013⟩
Accès au bibtex
https://arxiv.org/pdf/1310.8156 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
https://hal.inria.fr/hal-00787126/file/hhw-arxiv.pdf 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
https://hal.inria.fr/hal-00854426/file/DPLL-LK.pdf 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
https://hal.inria.fr/hal-00906789/file/Psyche.pdf 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
https://hal.inria.fr/hal-00937009/file/formula_linking.pdf 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
https://hal.inria.fr/hal-00906299/file/lics13.pdf 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
https://hal.inria.fr/hal-00906485/file/root.pdf 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
https://hal.inria.fr/hal-00906486/file/root.pdf 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
https://hal.inria.fr/hal-01285039/file/main.pdf BibTex
titre
Cut Elimination in Nested Sequents for Intuitionistic Modal Logics
auteur
Lutz Straßburger
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
https://hal.inria.fr/hal-00770678/file/nested-int-mod-fossacs13-HAL.pdf 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
https://hal.inria.fr/hal-00780774/file/diff_priv.pdf 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
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
https://hal.inria.fr/inria-00402942/file/hyll-report.pdf BibTex
titre
Automated reasoning techniques as proof-search in sequent calculus
auteur
Mahfuza Farooque
article
2013
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00939124/file/Main.pdf BibTex
titre
Sequent Calculi with procedure calls
auteur
Mahfuza Farooque, Stéphane Graham-Lengrand
article
2013
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-00779199/file/Main.pdf 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
Accès au texte intégral et bibtex
https://pastel.archives-ouvertes.fr/pastel-00961344/file/Farooque.pdf 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
Accès au texte intégral et bibtex
https://pastel.archives-ouvertes.fr/pastel-00913469/file/main.pdf BibTex
titre
Nested Deduction in Logical Foundations for Computation
auteur
Nicolas Guenot
article
Logic in Computer Science [cs.LO]. Ecole Polytechnique X, 2013. English
Accès au texte intégral et bibtex
https://pastel.archives-ouvertes.fr/pastel-00929908/file/thesis.pdf BibTex

Preprints, Working Papers, …

titre
Extracting Proofs from Tabled Proof Search
auteur
Dale Miller, Alwen Tiu
article
2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00863561/file/root.pdf BibTex
titre
Path Functors in Cat
auteur
François Lamarche
article
2013
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00831430/file/PathFunctorsInCat.pdf 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
https://hal.inria.fr/hal-00772727/file/fpc.pdf 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, Springer Verlag, 2012, 49 (2), pp.241-273. ⟨10.1007/s10817-011-9218-1⟩
Accès au bibtex
https://arxiv.org/pdf/0911.2993 BibTex
titre
Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus
auteur
Beniamino Accattoli, Delia Kesner
article
Logical Methods in Computer Science, Logical Methods in Computer Science Association, 2012, Logical Methods in Computer Science, 8 (1), pp.44. ⟨10.2168/LMCS-8(1:28)2012⟩
Accès au bibtex
https://arxiv.org/pdf/1203.0670 BibTex
titre
Extension without Cut
auteur
Lutz Straßburger
article
Annals of Pure and Applied Logic, Elsevier Masson, 2012, 163 (12), pp.1995-2007. ⟨10.1016/j.apal.2012.07.004⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00759215/file/psppp.pdf 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
https://hal.inria.fr/hal-00780337/file/CPP2012.pdf 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
https://hal.inria.fr/hal-00760118/file/deepcert.pdf 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
https://hal.inria.fr/hal-01112158/file/main.pdf BibTex
titre
Herbrand-Confluence for Cut Elimination in Classical First Order Logic
auteur
Stefan Hetzl, Lutz Straßburger
article
CSL 2012, Sep 2012, Fontainebleau, France. ⟨10.4230/LIPIcs.CSL.2012.320⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00759228/file/HerbrandConfluence.pdf 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
https://hal.inria.fr/hal-00772396/file/lkfexp.pdf 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
https://hal.inria.fr/hal-00776337/file/ascop.pdf 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
https://hal.inria.fr/hal-00780349/file/RTA2012-2.pdf 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
https://hal.inria.fr/hal-00780344/file/RTA2012-1.pdf 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
https://hal.inria.fr/hal-00780358/file/FLOPS2012.pdf 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
https://hal.inria.fr/hal-00665995/file/proof_example.pdf 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
https://hal.inria.fr/hal-00780361/file/LPAR2012.pdf BibTex

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
BibTex
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
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
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
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
https://hal.archives-ouvertes.fr/hal-00690577/file/Main.pdf 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
https://hal.archives-ouvertes.fr/hal-00844250/file/Main.pdf 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
https://hal.archives-ouvertes.fr/hal-00690044/file/Main.pdf 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
https://hal.inria.fr/hal-00690392/file/MainHal.pdf BibTex

2011

Journal articles

titre
Nominal Abstraction
auteur
Gacek Andrew, Dale Miller, Gopalan Nadathur
article
Journal of Information and Computation, Elsevier, 2011, 209 (1), pp.48-73
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00772606/file/nominal-abstraction.pdf 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, Logical Methods in Computer Science Association, 2011, 7 (1), pp.33. ⟨10.2168/LMCS-7(1:6)2011⟩
Accès au texte intégral et bibtex
https://hal.archives-ouvertes.fr/hal-01110478/file/TTSC09.pdf BibTex
titre
A System of Interaction and Structure IV: The Exponentials and Decomposition
auteur
Lutz Straßburger, Alessio Guglielmi
article
ACM Transactions on Computational Logic, Association for Computing Machinery, 2011, 12 (4), pp.23. ⟨10.1145/1970398.1970399⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00441214/file/SIS-IV.pdf BibTex
titre
From Deep Inference to Proof Nets via Cut Elimination
auteur
Lutz Straßburger
article
Journal of Logic and Computation, Oxford University Press (OUP), 2011, 21 (4), pp.589-624. ⟨http://logcom.oxfordjournals.org/content/21/4/589.full.pdf+html⟩. ⟨10.1093/logcom/exp047⟩
Accès au bibtex
BibTex
titre
A Focused Approach to Combining Logics
auteur
Chuck Liang, Dale Miller
article
Annals of Pure and Applied Logic, Elsevier Masson, 2011, ⟨10.1016/j.apal.2011.01.012⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00772736/file/lku.pdf BibTex
titre
A System of Interaction and Structure V: The Exponentials and Splitting
auteur
Alessio Guglielmi, Lutz Straßburger
article
Mathematical Structures in Computer Science, Cambridge University Press (CUP), 2011, pp.1-22. ⟨10.1017/S096012951100003X⟩
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00441254/file/NEL-splitting.pdf BibTex

Conference papers

titre
The Focused Calculus of Structures
auteur
Kaustuv Chaudhuri, Nicolas Guenot, Lutz Straßburger
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
https://hal.inria.fr/hal-00772420/file/paper88.pdf BibTex
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
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
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
https://hal.inria.fr/hal-00772722/file/cpp11.pdf BibTex

Habilitation à diriger des recherches

titre
Towards a Theory of Proofs of Classical Logic
auteur
Lutz Straßburger
article
Logic in Computer Science [cs.LO]. Université Paris-Diderot – Paris VII, 2011
Accès au texte intégral et bibtex
https://tel.archives-ouvertes.fr/tel-00772590/file/thehabil.pdf 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
https://hal.inria.fr/inria-00563331/file/main.pdf BibTex

2010

Journal articles

titre
Proof Search Specifications of the pi-calculus
auteur
Tiu Alwen, Dale Miller
article
ACM Transactions on Computational Logic, Association for Computing Machinery, 2010, 11 (2)
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00772571/file/tiu09tocl.pdf BibTex
titre
Proof and Refutation in MALL as a game
auteur
Olivier Delande, Dale Miller, Alexis Saurin
article
Annals of Pure and Applied Logic, Elsevier Masson, 2010, 161 (5), pp.654-672. ⟨10.1016/j.apal.2009.07.017⟩
Accès au bibtex
BibTex
titre
A framework for proof systems
auteur
Nigam Vivek, Dale Miller
article
Journal of Automated Reasoning, Springer Verlag, 2010, 45 (2)
Accès au texte intégral et bibtex
https://hal.inria.fr/hal-00772562/file/nigam-ijcar.pdf 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
https://hal.inria.fr/inria-00535948/file/magassign.pdf 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
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
https://hal.inria.fr/inria-00534865/file/clasint.pdf 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
https://hal.inria.fr/inria-00534821/file/tlaps.pdf 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
https://hal.inria.fr/hal-00772592/file/ijcar10.pdf 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
https://hal.inria.fr/hal-00772557/file/unity2010.pdf 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
https://hal.inria.fr/hal-00772599/file/aplas10.pdf BibTex

2009

Journal articles

titre
Focusing and Polarization in Linear, Intuitionistic, and Classical Logics
auteur
Liang Chuck, Dale Miller
article
Theoretical Computer Science, Elsevier, 2009, 410 (46), ⟨10.1016/j.tcs.2009.07.041⟩
Accès au bibtex
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
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
BibTex
titre
Expanding the Realm of Systematic Proof Theory
auteur
Agata Ciabattoni, Lutz Straßburger, 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
https://hal.inria.fr/inria-00436420/file/realm-finalforcsl.pdf BibTex
titre
Modular Sequent Systems for Modal Logic
auteur
Kai Brünnler, Lutz Straßburger
article
Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX’09, 2009, Oslo, Norway
Accès au bibtex
BibTex
titre
A Kleene Theorem for Forest Languages
auteur
Lutz Straßburger
article
Language and Automata Theory and Applications, LATA’09, 2009, Tarragona, Spain
Accès au bibtex
BibTex
titre
Some Observations on the Proof Theory of Second Order Propositional Multiplicative Linear Logic
auteur
Lutz Straßburger
article
Typed Lambda Calculi and Applications, TLCA’09, 2009, Brasilia, Brazil. ⟨10.1007/978-3-642-02273-9_23⟩
Accès au bibtex
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
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
BibTex
titre
Canonical Sequent Proofs via Multi-Focusing
auteur
Alexis Saurin, Kaustuv 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
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
https://hal.inria.fr/inria-00221221/file/RR-6431.pdf BibTex

2007

Conference papers

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
BibTex
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
https://hal.inria.fr/inria-00167231/file/csl07-014.pdf BibTex
titre
Deep Inference for Hybrid Logic
auteur
Lutz Straßburger
article
International Workshop on Hybrid Logic 2007 (HyLo 2007), Aug 2007, Dublin, Ireland
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00165998/file/hybrid.pdf BibTex
titre
A Characterisation of Medial as Rewriting Rule
auteur
Lutz Straßburger
article
RTA 2007, Jun 2007, Paris, France
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00165997/file/CharMedial.pdf BibTex

2006

Conference papers

titre
What could a Boolean category be?
auteur
Lutz Straßburger
article
Classical Logic and Computation 2006 (ICALP Workshop), Jul 2006, Venice, Italy
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00130504/file/medial-kurz.pdf 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
https://hal.inria.fr/inria-00167225/file/ppdp06-hal.pdf BibTex

Other publications

titre
On the Axiomatisation of Boolean Categories with and without Medial
auteur
Lutz Straßburger
article
2006
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00130508/file/medial.pdf BibTex

Reports

titre
Proof Nets and the Identity of Proofs
auteur
Lutz Straßburger
article
[Research Report] RR-6013, INRIA. 2006
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00107260/file/RR-6013.pdf 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
https://hal.inria.fr/inria-00201085/file/report.pdf BibTex
titre
From Deep Inference to Proof Nets
auteur
Lutz Straßburger
article
Structures and Deduction 2005 (ICALP Workshop), Jul 2005, Lisbon, Portugal
Accès au texte intégral et bibtex
https://hal.inria.fr/inria-00130501/file/deepnet.pdf 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
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
BibTex
titre
Constructing free Boolean categories
auteur
François Lamarche, Lutz Straßburger
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
https://hal.inria.fr/hal-00012296/file/FreeBool.pdf BibTex

Book sections

titre
What is a logic, and what is a proof ?
auteur
Lutz Straßburger
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
https://hal.inria.fr/inria-00130523/file/WhatLogicProof.pdf BibTex