Publications

2021

Article dans une revue

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

Article dans une revue

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

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

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

Communication dans un congrès

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

N°spécial de revue/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

Cours

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

Article dans une revue

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

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

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

Communication dans un congrès

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

Chapitre d’ouvrage

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

Document associé à des manifestations scientifiques

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

Rapport

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

Article dans une revue

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

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

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

Communication dans un congrès

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

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

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

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

Document associé à des manifestations scientifiques

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/Recueil des communications

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

Rapport

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

Article dans une revue

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

(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

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

Communication dans un congrès

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

Rapport

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

Pré-publication, Document de travail

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

Article dans une revue

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

Communication dans un congrès

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

Chapitre d’ouvrage

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

Ouvrages

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

Document associé à des manifestations scientifiques

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

Pré-publication, Document de travail

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

Article dans une revue

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

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

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

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

Communication dans un congrès

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

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

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

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

Chapitre d’ouvrage

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

HDR

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

Ouvrages

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

Pré-publication, Document de travail

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

Article dans une revue

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

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

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

Communication dans un congrès

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

Ouvrages

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

Rapport

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

Thèse

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

Pré-publication, Document de travail

titre

Extracting Proofs from Tabled Proof Search

auteur

Dale Miller, Alwen Tiu

article

2013

Accès au texte intégral et bibtex

titre

Path Functors in Cat

auteur

François Lamarche

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

Article dans une revue

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

Communication dans un congrès

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

Ouvrages

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

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

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

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

Rapport

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

Pré-publication, Document de travail

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

Article dans une revue

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

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

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

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

Communication dans un congrès

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

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

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

HDR

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

Pré-publication, Document de travail

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

Article dans une revue

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

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

Communication dans un congrès

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

Article dans une revue

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

Communication dans un congrès

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

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

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

2008

Communication dans un congrès

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

Rapport

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

Communication dans un congrès

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

Communication dans un congrès

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

Autre publication scientifique

titre

On the Axiomatisation of Boolean Categories with and without Medial

auteur

Lutz Strassburger

article

2006

Accès au texte intégral et bibtex

Rapport

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

Communication dans un congrès

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

Chapitre d’ouvrage

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