Bibliography

Major publications by the team in recent years

1K. Chaudhuri, F. Pfenning, G. Price.

A Logical Characterization of Forward and Backward Chaining in the Inverse Method, in: J. of Automated Reasoning, March 2008, vol. 40, n^o 2-3, p. 133–177. [ DOI : s10817-007-9091-0 ]

http://www.springerlink.com/content/b335r17728862pm2/fulltext.pdf
2O. Delande, D. Miller, A. Saurin.

Proof and refutation in MALL as a game, in: Annals of Pure and Applied Logic, February 2010, vol. 161, n^o 5, p. 654–672.

http://dx.doi.org/10.1016/j.apal.2009.07.017
3R. Dyckhoff, S. Lengrand.

Call-by-Value $λ$ -calculus and LJQ, in: Journal of Logic and Computation, 2007, vol. 17, n^o 6, p. 1109–1134.
4A. Gacek, D. Miller, G. Nadathur.

Nominal abstraction, in: Information and Computation, 2011, vol. 209, n^o 1, p. 48–73.

http://arxiv.org/abs/0908.1390
5A. Guglielmi, T. Gundersen, L. Straßburger.

Breaking Paths in Atomic Flows for Classical Logic, in: Proceedings of the 25th Annual IEEE Symposium on Logic in Computer Science (LICS 2010), Edinburgh, United Kingdom, July 2010, p. 284–293. [ DOI : 10.1109/LICS.2010.12 ]

http://www.lix.polytechnique.fr/~lutz/papers/AFII.pdf
6F. Lamarche, L. Straßburger.

Naming Proofs in Classical Propositional Logic, in: Typed Lambda Calculi and Applications, TLCA 2005, P. Urzyczyn (editor), LNCS, Springer-Verlag, 2005, vol. 3461, p. 246–261.
7S. Lengrand, R. Dyckhoff, J. McKinna.

A focused sequent calculus framework for proof search in Pure Type Systems, in: Logical Methods in Computer Science, 2010, To appear.
8C. Liang, D. Miller.

Focusing and Polarization in Linear, Intuitionistic, and Classical Logics, in: Theoretical Computer Science, 2009, vol. 410, n^o 46, p. 4747–4768.
9L. Straßburger.

On the Axiomatisation of Boolean Categories with and without Medial, in: Theory and Applications of Categories, 2007, vol. 18, n^o 18, p. 536–601.

http://arxiv.org/abs/cs.LO/0512086
10A. Tiu, D. Miller.

Proof Search Specifications of Bisimulation and Modal Logics for the $π$ -calculus, in: ACM Trans. on Computational Logic, 2010, vol. 11, n^o 2.

http://arxiv.org/abs/0805.2785

Publications of the year

Doctoral Dissertations and Habilitation Theses

11L. Straßburger.

Towards a Theory of Proofs of Classical Logic, Université Paris VII, 2011.

Articles in International Peer-Reviewed Journal

12A. Gacek, D. Miller, G. Nadathur.

Nominal abstraction, in: Information and Computation, 2011, vol. 209, n^o 1, p. 48–73.

http://arxiv.org/abs/0908.1390
13A. Guglielmi, L. Straßburger.

A system of interaction and structure V: the exponentials and splitting, in: Mathematical Structures in Computer Science, 2011, vol. 21, n^o 3, p. 563–584.
14C. Liang, D. Miller.

A Focused Approach to Combining Logics, in: Annals of Pure and Applied Logic, 2011, vol. 162, n^o 9, p. 679–697.

http://dx.doi.org/10.1016/j.apal.2011.01.012
15L. Straßburger, A. Guglielmi.

A system of interaction and structure IV: The exponentials and decomposition, in: ACM Trans. Comput. Log., 2011, vol. 12, n^o 4, 23 p.
16L. Straßburger.

From Deep Inference to Proof Nets via Cut Elimination, in: J. Log. Comput., 2011, vol. 21, n^o 4, p. 589–624.

International Conferences with Proceedings

17A. Bernadet, Stéphane. Lengrand.

Complexity of strongly normalising $λ$ -terms via non-idempotent intersection types, in: Proceedings of the 14th international conference on Foundations of Software Science and Computation Structures (FOSSACS'11), M. Hofmann (editor), LNCS, Springer-Verlag, March 2011, vol. 6604, p. 88–107.
18A. Bernadet, Stéphane. Lengrand.

Filter models: non-idempotent intersection types, orthogonality and polymorphism, in: Proceedings of the 20th Annual conference of the European Association for Computer Science Logic (CSL'11), M. Bezem (editor), Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, September 2011.
19K. Chaudhuri, N. Guenot, L. Straßburger.

The Focused Calculus of Structures, in: Computer Science Logic: 20th Annual Conference of the EACSL, Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, September 2011, p. 159–173. [ DOI : 10.4230/LIPIcs.CSL.2011.159 ]

http://drops.dagstuhl.de/opus/volltexte/2011/3229/pdf/16.pdf
20D. Miller.

A proposal for broad spectrum proof certificates, in: CPP: First International Conference on Certified Programs and Proofs, J.-P. Jouannaud, Z. Shao (editors), 2011.

Other Publications

21A. Brunel, O. Hermant, C. Houtmann.

Orthogonality and Boolean Algebras for Deduction Modulo.

http://hal.inria.fr/inria-00563331/en
22C. Liang, D. Miller.

Kripke Semantics and Proof Systems for Combining Intuitionistic Logic and Classical Logic, September 2011, Submitted.
23D. Miller.

Communicating and trusting proofs: The case for broad spectrum proof certificates, June 2011, Available from author's website.
24L. Méhats, L. Straßburger.

Non-crossing tree realizations of ordered degree sequences.

http://hal.inria.fr/hal-00649591
25L. Straßburger.

Nested sequent systems for intuitionistic modal logics, 2011, Invited talk at the workshop "Intuitionistic Modal Logics and Applications" (IMLA'11), part of 14th Congress of Logic, Methodology and Philosophy of Science, Nancy, July 19–26, 2011.
26L. Straßburger.

Towards a Theory of Proofs of Classical Logic, 2011, Invited talk at the workshop "Proof Systems at the Test of Computer Science: Foundational and Applicational Encounters", part of 14th Congress of Logic, Methodology and Philosophy of Science, Nancy, July 19–26, 2011.

References in notes

27S. Abramsky.

Computational Interpretations of Linear Logic, in: Theoretical Computer Science, 1993, vol. 111, p. 3–57.
28J.-M. Andreoli.

Logic Programming with Focusing Proofs in Linear Logic, in: Journal of Logic and Computation, 1992, vol. 2, n^o 3, p. 297–347.
29B. E. Aydemir, A. Bohannon, M. Fairbairn, J. N. Foster, B. C. Pierce, P. Sewell, D. Vytiniotis, G. Washburn, S. Weirich, S. Zdancewic.

Mechanized Metatheory for the Masses: The PoplMark Challenge, in: Theorem Proving in Higher Order Logics: 18th International Conference, LNCS, Springer-Verlag, 2005, p. 50–65.
30D. Baelde, D. Miller, Z. Snow.

Focused Inductive Theorem Proving, in: Fifth International Joint Conference on Automated Reasoning (IJCAR 2010), J. Giesl, R. Hähnle (editors), LNCS, 2010, n^o 6173, p. 278–292. [ DOI : 10.1007/978-3-642-14203-1 ]

http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/ijcar10.pdf
31K. Brünnler.

Deep Inference and Symmetry for Classical Proofs, Technische Universität Dresden, 2003.
32K. Brünnler.

Deep Sequent Systems for Modal Logic, in: Advances in Modal Logic, G. Governatori, I. Hodkinson, Y. Venema (editors), College Publications, 2006, vol. 6, p. 107–119.

http://www.aiml.net/volumes/volume6/Bruennler.ps
33K. Brünnler, L. Straßburger.

Modular Sequent Systems for Modal Logic, in: Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX'09, M. Giese, A. Waaler (editors), LNCS, Springer, 2009, vol. 5607, p. 152–166.
34K. Chaudhuri.

The Focused Inverse Method for Linear Logic, Carnegie Mellon University, December 2006, Technical report CMU-CS-06-162.

http://reports-archive.adm.cs.cmu.edu/anon/2006/CMU-CS-06-162.pdf
35K. Chaudhuri, J. Despeyroux.

A Hybrid Linear Logic for Constrained Transition Systems with Applications to Molecular Biology, INRIA, 2010.

http://hal.inria.fr/inria-00402942/
36K. Chaudhuri, D. Doligez, L. Lamport, S. Merz.

Verifying Safety Properties With the TLA $^{+}$ Proof System, in: Fifth International Joint Conference on Automated Reasoning (IJCAR 2010), Edinburgh, United Kingdom, J. Giesl, R. Hähnle (editors), LNAI, Springer, July 2010, vol. 6173, p. 142–148. [ DOI : 10.1007/978-3-642-14203-1_12 ]

http://hal.inria.fr/inria-00534821
37K. Chaudhuri, D. Miller, A. Saurin.

Canonical Sequent Proofs via Multi-Focusing, in: Fifth IFIP International Conference on Theoretical Computer Science, G. Ausiello, J. Karhumäki, G. Mauri, L. Ong (editors), IFIP International Federation for Information Processing, Boston: Springer, September 2008, vol. 273, p. 383–396.

http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/tcs08trackb.pdf
38A. Gacek, D. Miller, G. Nadathur.

Combining generic judgments with recursive definitions, in: 23th Symp. on Logic in Computer Science, F. Pfenning (editor), IEEE Computer Society Press, 2008, p. 33–44.

http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lics08a.pdf
39J.-Y. Girard.

Linear Logic, in: Theoretical Computer Science, 1987, vol. 50, p. 1–102.
40A. Guglielmi.

A System of Interaction and Structure, in: ACM Trans. on Computational Logic, 2007, vol. 8, n^o 1.
41A. Guglielmi, T. Gundersen.

Normalisation Control in Deep Inference Via Atomic Flows, in: Logical Methods in Computer Science, 2008, vol. 4, n^o 1:9, p. 1–36.

http://arxiv.org/abs/0709.1205
42A. Guglielmi, L. Straßburger.

Non-commutativity and MELL in the Calculus of Structures, in: Computer Science Logic, CSL 2001, L. Fribourg (editor), LNCS, Springer-Verlag, 2001, vol. 2142, p. 54–68.
43A. S. Henriksen.

Using LJF as a Framework for Proof Systems, University of Copenhagen, 2009.

http://hal.inria.fr/inria-00442159/en/
44P. Martin-Löf.

Constructive Mathematics and Computer Programming, in: Sixth International Congress for Logic, Methodology, and Philosophy of Science, Amsterdam, North-Holland, 1982, p. 153–175.
45R. McDowell, D. Miller.

Reasoning with Higher-Order Abstract Syntax in a Logical Framework, in: ACM Trans. on Computational Logic, 2002, vol. 3, n^o 1, p. 80–136.

http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/mcdowell01.pdf
46R. McDowell, D. Miller.

A Logic for Reasoning with Higher-Order Abstract Syntax, in: Proceedings, Twelfth Annual IEEE Symposium on Logic in Computer Science, Warsaw, Poland, G. Winskel (editor), IEEE Computer Society Press, July 1997, p. 434–445.
47D. Miller.

Forum: A Multiple-Conclusion Specification Logic, in: Theoretical Computer Science, September 1996, vol. 165, n^o 1, p. 201–232.
48D. Miller, G. Nadathur, F. Pfenning, A. Scedrov.

Uniform Proofs as a Foundation for Logic Programming, in: Annals of Pure and Applied Logic, 1991, vol. 51, p. 125–157.
49D. Miller, E. Pimentel.

Using linear logic to reason about sequent systems, in: International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, U. Egly, C. Fermüller (editors), LNCS, Springer, 2002, vol. 2381, p. 2–23.

http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/tableaux02.pdf
50D. Miller, A. Tiu.

A Proof Theory for Generic Judgments: An extended abstract, in: Proc. 18th IEEE Symposium on Logic in Computer Science (LICS 2003), IEEE, June 2003, p. 118–127.

http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lics03.pdf
51V. Nigam, D. Miller.

A framework for proof systems, March 2009, Extended version of IJCAR08 paper. Submitted.
52F. Pfenning, C. Schürmann.

System Description: Twelf — A Meta-Logical Framework for Deductive Systems, in: 16th Conference on Automated Deduction, Trento, H. Ganzinger (editor), LNAI, Springer, 1999, n^o 1632, p. 202–206.
53B. Pientka, J. Dunfield.

Beluga: A Framework for Programming and Reasoning with Deductive Systems (System Description), in: Fifth International Joint Conference on Automated Reasoning, J. Giesl, R. Hähnle (editors), LNCS, 2010, n^o 6173, p. 15–21.
54E. P. Robinson.

Proof Nets for Classical Logic, in: Journal of Logic and Computation, 2003, vol. 13, p. 777–797.
55L. Straßburger.

Linear Logic and Noncommutativity in the Calculus of Structures, Technische Universität Dresden, 2003.
56 The Coq Development Team.

The Coq Proof Assistant Version 8.3 Reference Manual, INRIA, October 2010.
57A. Tiu, D. Miller.

Proof Search Specifications of Bisimulation and Modal Logics for the $π$ -calculus, in: ACM Trans. on Computational Logic, 2010, vol. 11, n^o 2.

http://arxiv.org/abs/0805.2785

Previous |

Home