Bibliography

Major publications by the team in recent years

1K. 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 für Informatik, September 2011, p. 159–173. [ DOI : 10.4230/LIPIcs.CSL.2011.159 ]
2A. 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
3A. 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
4F. 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.
5S. 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.
6C. 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.
7C. 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. [ DOI : 10.1016/j.apal.2011.01.012 ]
8D. Miller.

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

http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/cpp11.pdf
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

Articles in International Peer-Reviewed Journals

11B. Accattoli, D. Kesner.

Preservation of Strong Normalisation modulo permutations for the structural lambda-calculus, in: Logical Methods in Computer Science, 2012, vol. 8, n^o 1. [ DOI : 10.2168/LMCS-8(1:28)2012 ]
12A. Gacek, D. Miller, G. Nadathur.

A two-level logic approach to reasoning about computations, in: J. of Automated Reasoning, 2012, vol. 49, n^o 2, p. 241–273. [ DOI : 10.1007/s10817-011-9218-1 ]

http://arxiv.org/abs/0911.2993
13F. Lamarche.

Modelling Martin Löf Type Theory in Categories, in: Journal of Applied Logic, June 2012, conference "Logic, Categories, Semantics, Bordeaux, France", scheduled to appear in June 2013.

http://hal.inria.fr/hal-00706562
14C. Liang, D. Miller.

Kripke Semantics and Proof Systems for Combining Intuitionistic Logic and Classical Logic, in: Annals of Pure and Applied Logic, February 2013, vol. 164, n^o 2, p. 86–111. [ DOI : 10.1016/j.apal.2012.09.005 ]
15L. Straßburger.

Extension without cut, in: Ann. Pure Appl. Logic, 2012, vol. 163, n^o 12, p. 1995–2007.

International Conferences with Proceedings

16B. Accattoli.

An Abstract Factorization Theorem for Explicit Substitutions, in: 23rd International Conference on Rewriting Techniques and Applications (RTA), Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2012, vol. 15, p. 6–21. [ DOI : 10.4230/LIPIcs.RTA.2012.6 ]
17B. Accattoli.

Proof pearl: Abella formalization of lambda calculus cube property, in: Second International Conference on Certified Programs and Proofs (CPP), Kyoto, Japan, LNCS, Springer, December 2012, vol. 7679, p. 173–187. [ DOI : 10.1007/978-3-642-35308-6_15 ]
18B. Accattoli, D. Kesner.

The Permutative $λ$ -Calculus, in: 18th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), LNCS, Springer, 2012, vol. 7180, p. 23–36. [ DOI : 10.1007/978-3-642-28717-6_5 ]
19B. Accattoli, U. D. Lago.

On the Invariance of the Unitary Cost Model for Head Reduction, in: 23rd International Conference on Rewriting Techniques and Applications (RTA), Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl–Leibniz-Zentrum für Informatik, 2012, vol. 15, p. 22–37. [ DOI : 10.4230/LIPIcs.RTA.2012.22 ]
20B. Accattoli, L. Paolini.

Call-by-Value Solvability, Revisited, in: Eleventh International Symposium on Functional and Logic Programming (FLOPS), LNCS, Springer, 2012, vol. 7294, p. 4–16. [ DOI : 10.1007/978-3-642-29822-6_4 ]
21K. Chaudhuri.

Compact Proof Certificates for Linear Logic, in: Proceedings of the Second Internatinal Conference on Certified Programs and Proofs (CPP), Kyoto, Japan, C. Hawblitzel, D. Miller (editors), LNCS, Springer, December 2012, vol. 7679, p. 208–223. [ DOI : 10.1007/978-3-642-35308-6_17 ]
22K. Chaudhuri, S. Hetzl, D. Miller.

A Systematic Approach to Canonicity in the Classical Sequent Calculus, in: Computer Science Logic (CSL'12): 21st Annual Conference of the EACSL, P. Cégielski, A. Durand (editors), Leibniz International Proceedings in Informatics (LIPIcs), Schloss Dagstuhl–Leibniz-Zentrum für Informatik, September 2012, vol. 16, p. 183–197. [ DOI : 10.4230/LIPIcs.CSL.2012.183 ]
23I. Gazeau, D. Miller, C. Palamidessi.

A non-local method for robustness analysis of floating point programs, in: QAPL - Tenth Workshop on Quantitative Aspects of Programming Languages, Tallinn, Estonia, M. Massink, H. Wiklicky (editors), Electronic Proceedings in Theoretical Computer Science, March 2012, vol. 85, p. 63–76. [ DOI : 10.4204/EPTCS.85.5 ]

http://hal.inria.fr/hal-00665995
24S. Hetzl.

Project Presentation: Algorithmic Structuring and Compression of Proofs (ASCOP), in: Conference on Intelligent Computer Mathematics (CICM) 2012, J. Jeuring, et al. (editors), Lecture Notes in Artificial Intelligence, Springer, 2012, vol. 7362, p. 437–441.
25S. Hetzl, L. Straßburger.

Herbrand-Confluence for Cut Elimination in Classical First Order Logic, in: Computer Science Logic (CSL'12) - 26th International Workshop/21st Annual Conference of the EACSL, CSL 2012, Fontainebleau, France, P. Cégielski, A. Durand (editors), LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, September 3-6 2012, vol. 16, p. 320–334.

Conferences without Proceedings

26B. Accattoli.

Proof nets and the call-by-vlaue lambda calculus, in: 7th Workshop on Logical and Semantic Frameworks, with Applications (LSFA), 2012.

Internal Reports

27M. Farooque, S. Lengrand.

A sequent calculus with procedure calls, Inria, December 2012.

http://hal.archives-ouvertes.fr/hal-00690577
28M. Farooque, S. Lengrand, A. Mahboubi.

Simulating the DPLL(T) procedure in a sequent calculus with focusing, Inria, April 2012.

http://hal.inria.fr/hal-00690392
29M. Farooque, S. Lengrand, A. Mahboubi.

Two simulations about DPLL(T), Inria, March 2012.

http://hal.archives-ouvertes.fr/hal-00690044

References in notes

30S. Abramsky.

Computational Interpretations of Linear Logic, in: Theoretical Computer Science, 1993, vol. 111, p. 3–57.
31B. Accattoli, D. Kesner.

The Structural ł-Calculus, in: CSL, 2010, p. 381–395. [ DOI : 10.1007/978-3-642-15205-4_30 ]
32J.-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.
33B. 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.
34D. 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
35K. 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
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.

Communicating and trusting proofs: The case for broad spectrum proof certificates, June 2011, Available from author's website.
48D. Miller.

Forum: A Multiple-Conclusion Specification Logic, in: Theoretical Computer Science, September 1996, vol. 165, n^o 1, p. 201–232.
49D. 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.
50D. 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
51D. 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
52V. Nigam, D. Miller.

A framework for proof systems, March 2009, Extended version of IJCAR08 paper. Submitted.
53F. 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.
54B. 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.
55E. P. Robinson.

Proof Nets for Classical Logic, in: Journal of Logic and Computation, 2003, vol. 13, p. 777–797.
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