EN FR
EN FR
PARSIFAL - 2018
PARSIFAL - 2018
Project-Team Parsifal
Team, Visitors, External Collaborators
Overall Objectives
Research Program
Application Domains
Highlights of the Year
New Software and Platforms
New Results
Partnerships and Cooperations
Dissemination
Bibliography


previous Previous | up Home


Bibliography

Major publications by the team in recent years
  • 1D. Baelde, K. Chaudhuri, A. Gacek, D. Miller, G. Nadathur, A. Tiu, Y. Wang.

    Abella: A System for Reasoning about Relational Specifications, in: Journal of Formalized Reasoning, 2014, vol. 7, no 2, pp. 1-89. [ DOI : 10.6092/issn.1972-5787/4650 ]

    https://hal.inria.fr/hal-01102709
  • 2A. 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, pp. 284–293. [ DOI : 10.1109/LICS.2010.12 ]

    http://www.lix.polytechnique.fr/~lutz/papers/AFII.pdf
Publications of the year

Articles in International Peer-Reviewed Journals

  • 3M. Acclavio.

    Proof Diagrams for Multiplicative Linear Logic: Syntax and Semantics, in: Journal of Automated Reasoning, May 2018. [ DOI : 10.1007/s10817-018-9466-4 ]

    https://hal.archives-ouvertes.fr/hal-01931400
  • 4F. Bour, T. Réfis, G. Scherer.

    Merlin: a language server for OCaml (experience report), in: Proceedings of the ACM on Programming Languages, July 2018, vol. 2, no ICFP, pp. 1 - 15, https://arxiv.org/abs/1807.06702. [ DOI : 10.1145/3236798 ]

    https://hal.inria.fr/hal-01929161
  • 5K. Chaudhuri, C. Olarte, E. Pimentel, J. Despeyroux.

    Hybrid Linear Logic, revisited, in: Mathematical Structures in Computer Science, 2019.

    https://hal.inria.fr/hal-01968154
  • 6O. Flückiger, G. Scherer, M.-H. Yee, A. Goel, A. Ahmed, J. Vitek.

    Correctness of Speculative Optimizations with Dynamic Deoptimization, in: Proceedings of the ACM on Programming Languages, 2018, vol. 2, no POPL, https://arxiv.org/abs/1711.03050. [ DOI : 10.1145/3158137 ]

    https://hal.inria.fr/hal-01646765
  • 7Q. Heath, D. Miller.

    A proof theory for model checking, in: Journal of Automated Reasoning, 2018. [ DOI : 10.1007/s10817-018-9475-3 ]

    https://hal.inria.fr/hal-01814006
  • 8J. Koppel, G. Scherer, A. Solar-Lezama.

    Capturing the Future by Replaying the Past Functional Pearl, in: Proceedings of the ACM on Programming Languages, July 2018, vol. 2, no ICFP, pp. 1 - 29. [ DOI : 10.1145/3236771 ]

    https://hal.inria.fr/hal-01929178
  • 9R. Kuznets, L. Straßburger.

    Maehara-style modal nested calculi, in: Archive for Mathematical Logic, July 2018. [ DOI : 10.1007/s00153-018-0636-1 ]

    https://hal.inria.fr/hal-01942240
  • 10D. Miller.

    Mechanized metatheory revisited, in: Journal of Automated Reasoning, 2018.

    https://hal.inria.fr/hal-01884210
  • 11L. Straßburger.

    Deep inference and expansion trees for second-order multiplicative linear logic, in: Mathematical Structures in Computer Science, November 2018, pp. 1-31. [ DOI : 10.1017/S0960129518000385 ]

    https://hal.inria.fr/hal-01942410

International Conferences with Proceedings

  • 12B. Accattoli, S. Graham-Lengrand, D. Kesner.

    Tight typings and split bounds, in: 23rd ACM International Conference on Functional Programming, St Louis, United States, M. Flatt (editor), September 2018, vol. 2, no ICFP, pp. 1 - 30, https://arxiv.org/abs/1807.02358. [ DOI : 10.1145/3236789 ]

    https://hal.archives-ouvertes.fr/hal-01936141
  • 13M. P. Bonacina, S. Graham-Lengrand, N. Shankar.

    Proofs in conflict-driven theory combination, in: Proceedings of the 7th International Conference on Certified Programs and Proofs (CPP'18), Los Angeles, United States, J. Andronick, A. Felty (editors), ACM Press, January 2018, vol. 18. [ DOI : 10.1145/3167096 ]

    https://hal.archives-ouvertes.fr/hal-01935595
  • 14K. Chaudhuri.

    A Two-Level Logic Perspective on (Simultaneous) Substitutions, in: CPP 2018 - Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, Los Angeles, United States, January 2018.

    https://hal.inria.fr/hal-01968139
  • 15K. Chaudhuri, U. Gérard, D. Miller.

    Computation-as-deduction in Abella: work in progress, in: 13th international Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Oxford, United Kingdom, July 2018.

    https://hal.inria.fr/hal-01806154
  • 16A. Condoluci, M. Manighetti.

    Admissible Tools in the Kitchen of Intuitionistic Logic, in: Seventh International Workshop on Classical Logic and Computation (CL&C 2018), Oxford, United Kingdom, Electronic Proceedings in Theoretical Computer Science, July 2018, vol. 281, pp. 10-23.

    https://hal.inria.fr/hal-01870112
  • 17U. Gérard, D. Miller.

    Functional programming with λ-tree syntax: a progress report, in: 13th international Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, Oxford, United Kingdom, July 2018.

    https://hal.inria.fr/hal-01806129
  • 18G. Scherer, M. New, N. Rioux, A. Ahmed.

    FabULous Interoperability for ML and a Linear Language, in: International Conference on Foundations of Software Science and Computation Structures (FoSSaCS), Thessaloniki, Greece, C. Baier, U. D. Lago (editors), FabOpen image in new windowous Interoperability for ML and a Linear Language, Springer, April 2018, vol. LNCS - Lecture Notes in Computer Science, no 10803, https://arxiv.org/abs/1707.04984. [ DOI : 10.1007/978-3-319-89366-2_8 ]

    https://hal.inria.fr/hal-01929158

National Conferences with Proceedings

Conferences without Proceedings

  • 21B. Accattoli.

    Proof Nets and the Linear Substitution Calculus, in: 15th International Colloquium on Theoretical Aspects of Computing (ICTAC 2018), Stellenbosch, South Africa, October 2018.

    https://hal.archives-ouvertes.fr/hal-01967532
  • 22B. Accattoli, G. Guerrieri.

    Types of Fireballs, in: 16th Asian Symposium on Programming Languages and System (APLAS 2018), Wellington, New Zealand, December 2018.

    https://hal.archives-ouvertes.fr/hal-01967531
  • 23F. Bobot, S. Graham-Lengrand, B. Marre, G. Bury.

    Centralizing equality reasoning in MCSAT, in: 16th International Workshop on Satisfiability Modulo Theories (SMT 2018), Oxford, United Kingdom, R. Dimitrova, V. D'Silva (editors), July 2018.

    https://hal.archives-ouvertes.fr/hal-01935591
  • 24S. Graham-Lengrand, M. Färber.

    Guiding SMT solvers with Monte Carlo Tree Search and neural networks, in: Third Conference on Artificial Intelligence and Theorem Proving (AITP'2018), Aussois, France, T. C. Hales, C. Kaliszyk, S. Schulz, J. Urban (editors), March 2018.

    https://hal.archives-ouvertes.fr/hal-01935578

Scientific Books (or Scientific Book chapters)

  • 25M. Acclavio, L. Straßburger.

    From Syntactic Proofs to Combinatorial Proofs, in: International Joint Conference on Automated Reasoning, IJCAR 2018, Springer, June 2018, pp. 481-497.

    https://hal.inria.fr/hal-01942275

Internal Reports

Other Publications

  • 28D. Miller.

    Influences between logic programming and proof theory, March 2018, HaPoP 2018: Fourth Symposium on the History and Philosophy of Programming.

    https://hal.inria.fr/hal-01900891
References in notes
  • 29J. A. Robinson, A. Voronkov (editors)

    Handbook of Automated Reasoning, Elsevier and MIT press, 2001.
  • 30S. Abramsky.

    Computational Interpretations of Linear Logic, in: Theoretical Computer Science, 1993, vol. 111, pp. 3–57.
  • 31B. Accattoli, U. Dal Lago.

    Beta reduction is invariant, indeed, in: 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), CSL-LICS '14, Vienna, Austria, July 14 - 18, 2014, 2014, pp. 8:1–8:10.

    http://doi.acm.org/10.1145/2603088.2603105
  • 32J.-M. Andreoli.

    Logic Programming with Focusing Proofs in Linear Logic, in: Journal of Logic and Computation, 1992, vol. 2, no 3, pp. 297–347.
  • 33D. 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, no 6173, pp. 278–292. [ DOI : 10.1007/978-3-642-14203-1 ]

    http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/ijcar10.pdf
  • 34G. E. Blelloch, J. Greiner.

    Parallelism in Sequential Functional Languages, in: Proceedings of the seventh international conference on Functional programming languages and computer architecture, FPCA 1995, La Jolla, California, USA, June 25-28, 1995, 1995, pp. 226–237.

    http://doi.acm.org/10.1145/224164.224210
  • 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, J. Despeyroux.

    A Hybrid Linear Logic for Constrained Transition Systems with Applications to Molecular Biology, Inria, 2010.
  • 37K. 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, pp. 159–173. [ DOI : 10.4230/LIPIcs.CSL.2011.159 ]

    http://drops.dagstuhl.de/opus/volltexte/2011/3229/pdf/16.pdf
  • 38K. Chaudhuri, S. Hetzl, D. Miller.

    A Multi-Focused Proof System Isomorphic to Expansion Proofs, in: Journal of Logic and Computation, June 2014. [ DOI : 10.1093/logcom/exu030 ]

    http://hal.inria.fr/hal-00937056
  • 39K. Chaudhuri, G. Reis.

    An adequate compositional encoding of bigraph structure in linear logic with subexponentials, in: Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), M. Davis, A. Fehnker, A. McIver, A. Voronkov (editors), LNCS, Springer, November 2015, vol. 9450, pp. 146–161. [ DOI : 10.1007/978-3-662-48899-7_11 ]

    http://chaudhuri.info/papers/lpar15bigraphs.pdf
  • 40K. Claessen, D. Rosén.

    SAT Modulo Intuitionistic Implications, in: Proc. of the the 20th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR'15), M. Davis, A. Fehnker, A. McIver, A. Voronkov (editors), LNCS, Springer-Verlag, November 2015, vol. 9450, pp. 622–637.

    http://dx.doi.org/10.1007/978-3-662-48899-7
  • 41C. Dross, S. Conchon, J. Kanig, A. Paskevich.

    Reasoning with Triggers, in: 10th Intern. Worksh. on Satisfiability Modulo Theories, SMT 2012, P. Fontaine, A. Goel (editors), EPiC Series, EasyChair, June 2012, vol. 20, pp. 22–31.

    http://smt2012.loria.fr/paper4.pdf
  • 42R. Dyckhoff.

    Contraction-free sequent calculi for intuitionistic logic, in: J. of Symbolic Logic, 1992, vol. 57, no 3, pp. 795–807.
  • 43A. 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, pp. 33–44.

    http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lics08a.pdf
  • 44A. Gacek, D. Miller, G. Nadathur.

    Nominal abstraction, in: Information and Computation, 2011, vol. 209, no 1, pp. 48–73.

    http://arxiv.org/abs/0908.1390
  • 45J.-Y. Girard.

    Linear Logic, in: Theoretical Computer Science, 1987, vol. 50, pp. 1–102.
  • 46S. Graham-Lengrand, R. Dyckhoff, J. McKinna.

    A Focused Sequent Calculus Framework for Proof Search in Pure Type Systems, in: Logical Methods in Computer Science, 2011, vol. 7, no 1.

    http://www.lix.polytechnique.fr/~lengrand/Work/Reports/TTSC09.pdf
  • 47S. Graham-Lengrand.

    Slot Machines: an approach to the Strategy Challenge in SMT solving (presentation only), in: 13th International Workshop on Satisfiability Modulo Theories, San Francisco, United States, July 2015.

    https://hal.inria.fr/hal-01211209
  • 48A. Guglielmi.

    A System of Interaction and Structure, in: ACM Trans. on Computational Logic, 2007, vol. 8, no 1.
  • 49A. Guglielmi, T. Gundersen.

    Normalisation Control in Deep Inference Via Atomic Flows, in: Logical Methods in Computer Science, 2008, vol. 4, no 1:9, pp. 1–36.

    http://arxiv.org/abs/0709.1205
  • 50A. 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, pp. 54–68.
  • 51J. Hudelmaier.

    Bounds for Cut Elimination in Intuitionistic Logic, Universität Tübingen, 1989.
  • 52D. Hughes.

    Proofs Without Syntax, in: Annals of Mathematics, 2006, vol. 164, no 3, pp. 1065–1076.
  • 53D. Jovanović, C. Barrett, L. de Moura.

    The Design and Implementation of the Model Constructing Satisfiability Calculus, in: Proc. of the 13th Int. Conf. on Formal Methods In Computer-Aided Design (FMCAD '13), FMCAD Inc., 2013, Portland, Oregon.

    http://www.cs.nyu.edu/~barrett/pubs/JBdM13.pdf
  • 54F. Lamarche, L. Straßburger.

    Naming Proofs in Classical Propositional Logic, in: Typed Lambda Calculi and Applications, TLCA 2005, P. Urzyczyn (editor), LNCS, Springer, 2005, vol. 3461, pp. 246–261.
  • 55C. Liang, D. Miller.

    Focusing and Polarization in Linear, Intuitionistic, and Classical Logics, in: Theoretical Computer Science, 2009, vol. 410, no 46, pp. 4747–4768.

    http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/tcs09.pdf
  • 56C. Liang, D. Miller.

    A Focused Approach to Combining Logics, in: Annals of Pure and Applied Logic, 2011, vol. 162, no 9, pp. 679–697.

    http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lku.pdf
  • 57P. Martin-Löf.

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

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

    http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/mcdowell01.pdf
  • 59R. 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, pp. 434–445.
  • 60D. Miller.

    Forum: A Multiple-Conclusion Specification Logic, in: Theoretical Computer Science, September 1996, vol. 165, no 1, pp. 201–232.
  • 61D. 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, pp. 125–157.
  • 62D. 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, pp. 118–127.

    http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lics03.pdf
  • 63R. Milner.

    LCF: A Way of Doing Proofs with a Machine, in: Proc. of the 8th Intern. Symp. on the Mathematical Foundations of Computer Science, J. Becvár (editor), LNCS, Springer, 1979, vol. 74, pp. 146-159.
  • 64G. Nelson, D. C. Oppen.

    Simplification by Cooperating Decision Procedures, in: ACM Press Trans. on Program. Lang. and Syst., October 1979, vol. 1, no 2, pp. 245–257.

    http://dx.doi.org/10.1145/357073.357079
  • 65C. Olarte, V. Nigam, E. Pimentel.

    Subexponential concurrent constraint programming, in: Theoretical Computer Science, 2015.

    http://dx.doi.org/10.1016/j.tcs.2015.06.031
  • 66F. 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, no 1632, pp. 202–206.
  • 67B. 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, no 6173, pp. 15–21.
  • 68E. P. Robinson.

    Proof Nets for Classical Logic, in: Journal of Logic and Computation, 2003, vol. 13, pp. 777–797.
  • 69R. E. Shostak.

    Deciding Combinations of Theories, in: J. ACM, 1984, vol. 31, no 1, pp. 1–12.

    http://dx.doi.org/10.1145/2422.322411
  • 70The Coq Development Team.

    The Coq Proof Assistant Version 8.3 Reference Manual, Inria, October 2010.
  • 71A. Tiu, D. Miller.

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

    http://arxiv.org/abs/0805.2785
  • 72N. N. Vorob'ev.

    A new algorithm for derivability in the constructive propositional calculus, in: Amer. Math. Soc. Transl., 1970, vol. 94, no 2, pp. 37–71.
  • 73L. M. de Moura, D. Jovanović.

    A Model-Constructing Satisfiability Calculus, in: Proc. of the 14th Int. Conf. on Verification, Model Checking, and Abstract Interpretation (VMCAI'13), R. Giacobazzi, J. Berdine, I. Mastroeni (editors), LNCS, Springer-Verlag, 2013, vol. 7737, pp. 1–12.

    http://dx.doi.org/10.1007/978-3-642-35873-9_1
  • 74L. M. de Moura, G. O. Passmore.

    The Strategy Challenge in SMT Solving, in: Automated Reasoning and Mathematics - Essays in Memory of William W. McCune, M. P. Bonacina, M. E. Stickel (editors), LNCS, Springer, 2013, vol. 7788, pp. 15–44. [ DOI : 10.1007/978-3-642-36675-8_2 ]

    http://dx.doi.org/10.1007/978-3-642-36675-8


previous Previous | up Home