PARSIFAL team publications

2013

In peer reviewed journal articles

Titre

A formal framework for specifying sequent calculus proof systems

Auteurs

Dale Miller ; Pimentel Elaine

Détail

Theoretical Computer Science, Elsevier, 2013, pp. 98-116

Accès au bibtex

Titre

Kripke Semantics and Proof Systems for Combining Intuitionistic Logic and Classical Logic

Auteurs

Liang Chuck ; Dale Miller

Détail

Annals of Pure and Applied Logic, Elsevier, 2013, 164 (2), pp. 86-111

Accès au texte intégral et bibtex

Research reports

Titre

Sequent Calculi with procedure calls

Auteurs

Mahfuza Farooque; Stéphane Graham-Lengrand

Détail

[Report], 2013

Accès au texte intégral et bibtex

Titre

Preserving differential privacy under finite-precision semantics

Auteurs

Ivan Gazeau ; Dale Miller; Catuscia Palamidessi

Détail

[Research Report], 2013

Accès au texte intégral et bibtex

Documents without publication reference

Titre

Reasoning About Higher-Order Relational Specifications

Auteurs

Yuting Wang; Kaustuv Chaudhuri ; Andrew Gacek; Gopalan Nadathur

Détail

Feb. 2013

Accès au texte intégral et bibtex

Titre

Communicating and trusting proofs: The case for foundational proof certificates

Auteurs

Dale Miller

Détail

Jan. 2013. To appear in the Proceedings of the 14th Congress of Logic, Methodology and Philosophy of Science in Nancy, France, 19-26 July 2011.

Accès au texte intégral et bibtex

2012

In peer reviewed journal articles

Titre

A two-level logic approach to reasoning about computations

Auteurs

Andrew Gacek; Dale Miller; Gopalan Nadathur

Détail

Journal of Automated Reasoning, Elsevier, 2012, 49 (2), pp. 241-273

Accès au bibtex

In peer reviewed conference proceedings

Titre

Compact Proof Certificates for Linear Logic

Auteurs

Kaustuv Chaudhuri

Détail

Chris Hawblitzel and Dale Miller. Second International Conference on Certified Programs and Proofs, Dec 2012, Kyoto, Japan. Springer, Lecture Notes in Computer Science (LNCS), 7679, pp. 208-223

Accès au texte intégral et bibtex

Titre

A Systematic Approach to Canonicity in the Classical Sequent Calculus

Auteurs

Kaustuv Chaudhuri ; Stefan Hetzl ; Dale Miller

Détail

Patrick Cégielski and Arnaud Durand. 21st EACSL Annual Conference on Computer Science Logic, Sep 2012, Fontainebleau, France. Leibniz International Proceedings in Informatics (LIPIcs), 16, pp. 183-197

Accès au texte intégral et bibtex

Titre

Project Presentation: Algorithmic Structuring and Compression of Proofs (ASCOP)

Auteurs

Stefan Hetzl

Détail

Conferences on Intelligent Computer Mathematics (CICM) 2012, Jul 2012, Bremen, Germany.

Accès au texte intégral et bibtex

Titre

Modelling Martin Löf Type Theory in Categories

Auteurs

François Lamarche

Détail

Ch. Retoré and J. Gilibert. Logic, Categories, Semantics, special issue of J. of Applied Logic, Nov 2010, Bordeaux, France. Elsevier North-Holland, Journal of Applied Logic (special issue), scheduled to appear in June 2013, 2012

Accès au texte intégral et bibtex

Titre

A non-local method for robustness analysis of floating point programs

Auteurs

Ivan Gazeau ; Dale Miller ; Catuscia Palamidessi

Détail

Mieke Massink and Herbert Wiklicky. QAPL - Tenth Workshop on Quantitative Aspects of Programming Languages, Mar 2012, Tallinn, Estonia.

Accès au texte intégral et bibtex

Scientific Books

Titre

Programming with Higher-Order Logic

Auteurs

Dale Miller ; Nadathur Gopalan

Détail

Cambridge University Press, pp. 320, 2012, 9780521879408

Accès au bibtex

Titre

Automated Reasoning: 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 2012, Proceedings

Auteurs

Gramlich Bernhard ; Dale Miller ; Sattler Uli

Détail

7364. Springer, pp. 568, 2012, lnai

Accès au bibtex

Titre

CPP 2012: Second International Conference on Certified Programs and Proofs

Auteurs

Hawblitzel Chris ; Dale Miller

Détail

7679. Springer, pp. 305, 2012, lncs

Accès au bibtex

Titre

Proceedings 8th Workshop on Fixed Points in Computer Science

Auteurs

Dale Miller ; Zoltán Ésik

Détail

77. Electronic Proceedings in Theoretical Computer Science, pp. 61, 2012

Accès au bibtex

Research reports

Titre

A sequent calculus with procedure calls

Auteurs

Mahfuza Farooque; Stéphane Lengrand

Détail

[Report], 2012

Accès au texte intégral et bibtex

Titre

Two simulations about DPLL(T)

Auteurs

Mahfuza Farooque; Stéphane Lengrand ; Assia Mahboubi

Détail

[Report], 2012

Accès au bibtex

Documents without publication reference

Titre

Simulating the DPLL(T ) procedure in a sequent calculus with focusing

Auteurs

Mahfuza Farooque; Stéphane Lengrand ; Assia Mahboubi

Détail

Apr. 2012

Accès au texte intégral et bibtex

2011

In peer reviewed journal articles

Titre

A Focused Approach to Combining Logics

Auteurs

Chuck Liang ; Dale Miller

Détail

Annals of Pure and Applied Logic, Elsevier, 2011

Accès au texte intégral et bibtex

Titre

A System of Interaction and Structure IV: The Exponentials and Decomposition

Auteurs

Lutz Straßburger; Alessio Guglielmi

Détail

ACM Trans. Comput. Log., ACM, 2011, 12 (4), pp. 23

Accès au bibtex

In peer reviewed conference proceedings

Titre

The Focused Calculus of Structures

Auteurs

Kaustuv Chaudhuri ; Nicolas Guenot; Lutz Straßburger

Détail

Marc Bezem. 20th EACSL Annual Conference on Computer Science Logic, Sep 2011, Bergen, Norway. Leibniz International Proceedings in Informatics (LIPIcs), 12, pp. 159-173

Accès au texte intégral et bibtex

Titre

A proposal for broad spectrum proof certificates

Auteurs

Dale Miller

Détail

CPP 2011 - First International Conference on Certified Proofs and Programs, 2011, Kenting, Taiwan, Province Of China.

Accès au texte intégral et bibtex

Documents without publication reference

Titre

Orthogonality and Boolean Algebras for Deduction Modulo

Auteurs

Alois Brunel; Olivier Hermant; Clement Houtmann

Détail

Feb. 2011

Accès au texte intégral et bibtex

2010

In peer reviewed journal articles

Titre

Proof and Refutation in MALL as a game

Auteurs

Olivier Delande; Dale Miller; Alexis Saurin

Détail

Annals of Pure and Applied Logic, 2010, 161 (5), pp. 654-672

Accès au bibtex

Titre

A framework for proof systems

Auteurs

Nigam Vivek ; Dale Miller

Détail

Journal of Automated Reasoning, Elsevier, 2010, 45 (2)

Accès au texte intégral et bibtex

Titre

Proof Search Specifications of the pi-calculus

Auteurs

Tiu Alwen ; Dale Miller

Détail

ACM Transactions on Computational Logic, ACM, 2010, 11 (2)

Accès au texte intégral et bibtex

Titre

Nominal Abstraction

Auteurs

Gacek Andrew ; Dale Miller ; Gopalan Nadathur

Détail

Journal of Information and Computation, Elsevier, 2010

Accès au texte intégral et bibtex

In peer reviewed conference proceedings

Titre

Finding Unity in Computational Logic

Auteurs

Dale Miller

Détail

ACM-BCS Visions of Computer Science, 2010, Edinburgh, United Kingdom.

Accès au texte intégral et bibtex

Titre

Focused Inductive Theorem Proving

Auteurs

David Baelde ; Dale Miller ; Zachary Snow

Détail

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

Auteurs

Dale Miller

Détail

APLAS 2010: Eighth Asian Symposium on Programming Languages and Systems, 2010, Shanghai, China.

Accès au texte intégral et bibtex

Titre

The TLA+ Proof System: Building a Heterogeneous Verification Platform

Auteurs

Kaustuv Chaudhuri; Damien Doligez; Leslie Lamport; Stephan Merz

Détail

Ana Cavalcanti and David Déharbe and Marie-Claude Gaudel and Jim Woodcock. International Conference on Theoretical Aspects of Computing - ICTAC 2010, Sep 2010, Natal, Brazil. Springer, Theoretical Aspects of Computing - ICTAC 2010, 6255, pp. 44, Lecture Notes in Computer Science

Accès au bibtex

Titre

Verifying Safety Properties With the TLA+ Proof System

Auteurs

Kaustuv Chaudhuri; Damien Doligez; Leslie Lamport; Stephan Merz

Détail

Jürgen Giesl and Reiner Haehnle. Fifth International Joint Conference on Automated Reasoning - IJCAR 2010, Jul 2010, Edinburgh, United Kingdom. Springer, Automated Reasoning 5th International Joint Conference, IJCAR 2010 Edinburgh, UK, July 16-19, 2010 Proceedings, 6173, pp. 142-148, Lecture Notes in Artificial Intelligence

Accès au texte intégral et bibtex

Titre

Classical and Intuitionistic Subexponential Logics are Equally Expressive

Auteurs

Kaustuv Chaudhuri

Détail

Anuj Dawar and Helmut Veith. Computer Science Logic, Aug 2010, Brno, Czech Republic. Springer, LNCS, 6247, pp. 185-199

Accès au texte intégral et bibtex

Titre

Magically Constraining the Inverse Method Using Dynamic Polarity Assignment

Auteurs

Kaustuv Chaudhuri

Détail

Christian Fermueller and Andrei Voronkov. Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), Oct 2010, Yogyakarta, Indonesia. Springer, LNCS, 6397, pp. 202-216

Accès au texte intégral et bibtex

Research reports

Titre

A Hybrid Linear Logic for Constrained Transition Systems with Applications to Molecular Biology

Auteurs

Kaustuv Chaudhuri; Joelle Despeyroux

Détail

[Research Report], 2010, pp. 30

Accès au texte intégral et bibtex

2009

In peer reviewed journal articles

Titre

Focusing and Polarization in Linear, Intuitionistic, and Classical Logics

Auteurs

Liang Chuck ; Dale Miller

Détail

Theoretical Computer Science, Elsevier, 2009, 410 (46)

Accès au bibtex

In peer reviewed conference proceedings

Titre

Algorithmic specifications in linear logic with subexponentials

Auteurs

Nigam Vivek ; Dale Miller

Détail

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

Auteurs

Liang Chuck ; Dale Miller

Détail

LICS 2009 - Twenty-Fourth Annual IEEE Symposium on LOGIC IN COMPUTER SCIENCE, Aug 2009, Los Angeles, United States.

Accès au bibtex

Titre

Modular Sequent Systems for Modal Logic

Auteurs

Kai Brünnler; Lutz Straßburger

Détail

Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX'09, 2009, Oslo, Norway.

Accès au bibtex

Titre

A Kleene Theorem for Forest Languages

Auteurs

Lutz Straßburger

Détail

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

Auteurs

Lutz Straßburger

Détail

Typed Lambda Calculi and Applications, TLCA'09, 2009, Brasilia, Brazil.

Accès au bibtex

Titre

Expanding the Realm of Systematic Proof Theory

Auteurs

Agata Ciabattoni; Lutz Straßburger; Kazushige Terui

Détail

Computer Science Logic, CSL'09, 2009, Coimbra, Portugal.

Accès au texte intégral et bibtex

Documents without publication reference

Titre

A System of Interaction and Structure V: The Exponentials and Splitting

Auteurs

Alessio Guglielmi; Lutz Straßburger

Détail

2009

Accès au texte intégral et bibtex

2008

In peer reviewed conference proceedings

Titre

Canonical Sequent Proofs via Multi-Focusing

Auteurs

Alexis Saurin; Kaustuv Chaudhuri; Dale Miller

Détail

Fifth IFIP International Conference On Theoretical Computer Science - TCS 2008, IFIP 20th World Computer Congress, Sep 2008, Milano, Italy. pp. 383-396

Accès au bibtex

Titre

Towards Ludics Programming: Interactive Proof Search

Auteurs

Alexis Saurin

Détail

24th International Conference on Logic Programming - ICLP 2008, Dec 2008, Udine, Italy. Springer, pp. 253-268, Lecture notes in computer science

Accès au bibtex

Titre

On the Relations between the Syntactic Theories of $\lambda\mu$-Calculi

Auteurs

Alexis Saurin

Détail

17th EACSL Annual Conference on Computer Science Logic - CSL 2008, Sep 2008, Bertinoro, Italy. Springer, 5213, pp. 154-168, Lecture notes in computer science

Accès au bibtex

Research reports

Titre

Stream Associative Nets and Lambda-mu-calculus

Auteurs

Michele Pagani; Alexis Saurin

Détail

[Research Report], 2008, pp. 48. RR-6431

Accès au texte intégral et bibtex

2007

In peer reviewed conference proceedings

Titre

Focusing and Polarization in Intuitionistic Logic

Auteurs

Chuck Liang; Dale Miller

Détail

Computer Science Logic, Sep 2007, Lausanne, Switzerland.

Accès au texte intégral et bibtex

Titre

A Characterisation of Medial as Rewriting Rule

Auteurs

Lutz Straßburger

Détail

RTA 2007, Jun 2007, Paris, France.

Accès au texte intégral et bibtex

Titre

From Proofs to Focused Proofs: A Modular Proof of Focalization in Linear Logic

Auteurs

Alexis Saurin; Dale Miller

Détail

16th EACSL Annual Conference on Computer Science and Logic - CSL 2007, Sep 2007, Lausanne, Switzerland. Springer, pp. 405-419, Lecture notes in computer science

Accès au bibtex

Congress communications

Titre

Deep Inference for Hybrid Logic

Auteurs

Lutz Straßburger

Détail

International Workshop on Hybrid Logic 2007 (HyLo 2007), Aug 2007, Dublin, Ireland.

Accès au texte intégral et bibtex

2006

In peer reviewed conference proceedings

Titre

Collection analysis for Horn clause programs

Auteurs

Dale Miller

Détail

International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, Jul 2006, Venice, Italy.

Accès au texte intégral et bibtex

Titre

A game semantics for proof search, preliminary results

Auteurs

Alexis Saurin; Dale Miller

Détail

Twenty-first Conference on the Mathematical Foundations of Programming Semantics - MFPS XXI, May 2005, Birmingham, United Kingdom. 155, pp. 543-563, 2006

Accès au bibtex

Titre

What could a Boolean category be?

Auteurs

Lutz Straßburger

Détail

Classical Logic and Computation 2006 (ICALP Workshop), Jul 2006, Venice, Italy.

Accès au texte intégral et bibtex

Titre

A Congruence Format for Name-passing Calculi

Auteurs

Axelle Ziegler; Dale Miller; Catuscia Palamidessi

Détail

Peter Mosses and Irek Ulidowski. 2nd Workshop on Structural Operational Semantics (SOS'05), Jul 2005, Lisboa, Portugal. Elsevier, Proceedings of the 2nd Workshop on Structural Operational Semantics, 156 (1), pp. 169-189, 2006, Electronic Notes in Theoretical Computer Science

Accès au texte intégral et bibtex

Other publications

Titre

On the Axiomatisation of Boolean Categories with and without Medial

Auteurs

Lutz Straßburger

Détail

2006

Accès au texte intégral et bibtex

Research reports

Titre

Proof Nets and the Identity of Proofs

Auteurs

Lutz Straßburger

Détail

[Research Report], 2006. RR-6013

Accès au texte intégral et bibtex

2005

In peer reviewed conference proceedings

Titre

Constructing free Boolean categories

Auteurs

François Lamarche; Lutz Straßburger

Détail

20th Annual IEEE Symposium on Logic in Computer Science - LICS 2005, May 2005, Chicago/USA, United States. pp. 209- 218

Accès au texte intégral et bibtex

Titre

Separation with streams in the $\Lambda\mu$-calculus

Auteurs

Alexis Saurin

Détail

20th Annual IEEE Symposium on Logic In Computer Science - LICS 2005, Jun 2005, Chicago, United States. IEEE, pp. 356-365

Accès au bibtex

Titre

From Deep Inference to Proof Nets

Auteurs

Lutz Straßburger

Détail

Structures and Deduction 2005 (ICALP Workshop), Jul 2005, Lisbon, Portugal.

Accès au texte intégral et bibtex

Scientific Book chapters

Titre

What is a logic, and what is a proof ?

Auteurs

Lutz Straßburger

Détail

Jean-Yves Beziau. Logica Universalis, Birkhäuser, pp. 135-145, 2005, 978-3-7643-7259-0

Accès au texte intégral et bibtex