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, n^o 2, pp. 1-89. [ DOI : 10.6092/issn.1972-5787/4650 ]

https://hal.inria.fr/hal-01102709
2K. 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.

http://drops.dagstuhl.de/opus/frontdoor.php?source_opus=3229
3M. Farooque, S. Graham-Lengrand, A. Mahboubi.

A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus, in: Proceedings of the 2013 International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2013), A. Momigliano, B. Pientka, R. Pollack (editors), ACM Press, September 2013.

http://dx.doi.org/10.1145/2503887.2503892
4A. Gacek, D. Miller, G. Nadathur.

Nominal abstraction, in: Information and Computation, 2011, vol. 209, n^o 1, pp. 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, pp. 284–293. [ DOI : 10.1109/LICS.2010.12 ]

http://www.lix.polytechnique.fr/~lutz/papers/AFII.pdf
6C. Liang, D. Miller.

Focusing and Polarization in Linear, Intuitionistic, and Classical Logics, in: Theoretical Computer Science, 2009, vol. 410, n^o 46, pp. 4747–4768.
7C. Liang, D. Miller.

A Focused Approach to Combining Logics, in: Annals of Pure and Appl. Logic, 2011, vol. 162, n^o 9, pp. 679–697. [ DOI : 10.1016/j.apal.2011.01.012 ]

http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lku.pdf
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, pp. 54–69.

http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/cpp11.pdf
9L. Straßburger.

Extension without Cut, in: Annals of Pure and Appl. Logic, 2012, vol. 163, n^o 12, pp. 1995–2007.
10L. Straßburger.

Combinatorial Flows and Their Normalisation, in: 2nd International Conference on Formal Structures for Computation and Deduction, FSCD 2017, September 3-9, 2017, Oxford, UK, D. Miller (editor), LIPIcs, Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik, 2017, vol. 84, pp. 31:1–31:17.
11A. 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

12B. Accattoli, C. Sacerdoti Coen.

On the Value of Variables, in: Information and Computation, August 2017, vol. 255, pp. 224 - 242. [ DOI : 10.1016/j.ic.2017.01.003 ]

https://hal.archives-ouvertes.fr/hal-01675373
13Z. Chihani, D. Miller, F. Renaud.

A Semantic Framework for Proof Evidence, in: Journal of Automated Reasoning, 2017, vol. 59, n^o 3, pp. 287-330. [ DOI : 10.1007/s10817-016-9380-6 ]

https://hal.inria.fr/hal-01390912
14O. 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, 2017, https://arxiv.org/abs/1711.03050, forthcoming. [ DOI : 10.1145/3158137 ]

https://hal.inria.fr/hal-01646765
15D. Miller.

Proof Checking and Logic Programming, in: Formal Aspects of Computing, 2017, vol. 29, n^o 3, pp. 383-399. [ DOI : 10.1007/s00165-016-0393-z ]

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

Articles in Non Peer-Reviewed Journals

16D. Ilik.

Perspectives for proof unwinding by programming languages techniques, in: IfColog Journal of Logics and their Applications (FLAP), November 2017, vol. 4, n^o 10, pp. 3487-3508, https://arxiv.org/abs/1605.09177.

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

International Conferences with Proceedings

17R. Blanco, Z. Chihani, D. Miller.

Translating Between Implicit and Explicit Versions of Proof, in: CADE 26 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 2017.

https://hal.inria.fr/hal-01645016
18R. Blanco, D. Miller, A. Momigliano.

Property-Based Testing via Proof Reconstruction Work-in-progress, in: LFMTP 17: Logical Frameworks and Meta-Languages: Theory and Practice, Oxford, United Kingdom, September 2017.

https://hal.inria.fr/hal-01646788
19M. P. Bonacina, S. Graham-Lengrand, N. Shankar.

Satisfiability Modulo Theories and Assignments, in: CADE 2017 - 26th International Conference on Automated Deduction, Gothenburg, Sweden, August 2017. [ DOI : 10.1007/978-3-319-63046-5_4 ]

https://hal.archives-ouvertes.fr/hal-01615830
20P. Bruscoli, L. Straßburger.

On the Length of Medial-Switch-Mix Derivations, in: WoLLIC 2017 - Logic, Language, Information, and Computation, London, United Kingdom, July 2017.

https://hal.inria.fr/hal-01635933
21S. Graham-Lengrand, D. Jovanović.

An MCSAT treatment of Bit-Vectors (preliminary report), in: SMT 2017 - 15th International Workshop on Satisfiability Modulo Theories, Heidelberg, Germany, July 2017.

https://hal.archives-ouvertes.fr/hal-01615837
22U. Gérard, D. Miller.

Separating Functional Computation from Relations, in: 26th EACSL Annual Conference on Computer Science Logic (CSL 2017), Stockholm, Sweden, LIPIcs, August 2017, vol. 82, n^o 23, pp. 23:1–23:17.

https://hal.inria.fr/hal-01615683
23D. Ilik.

On the exp-log normal form of types: Decomposing extensional equality and representing terms compactly, in: Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, Paris, France, January 2017, pp. 387-399, https://arxiv.org/abs/1502.04634.

https://hal.inria.fr/hal-01167162
24S. Marin, L. Straßburger.

Proof theory for indexed nested sequents, in: TABLEAUX 2017 - Automated Reasoning with Analytic Tableaux and Related Methods, Brasilia, Brazil, LNCS, September 2017, vol. 10501, pp. 81-97.

https://hal.inria.fr/hal-01635935
25D. Miller.

Linear logic as a logical framework, in: Proceedings of Structures and Deduction (SD) 2017, Oxford, United Kingdom, September 2017.

https://hal.archives-ouvertes.fr/hal-01615664
26D. Miller.

Mechanized Metatheory Revisited: An Extended Abstract , in: Post-proceedings of TYPES 2016, Novi Sad, Serbia, 2017. [ DOI : 10.4230/LIPIcs ]

https://hal.inria.fr/hal-01615681
27G. Scherer.

Deciding equivalence with sums and the empty type, in: POPL 2017, Paris, France, POPL 2017- Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, January 2017, https://arxiv.org/abs/1610.01213 - This work was presented at POPL 2017: Principles of Programming Languages. [ DOI : 10.01213 ]

https://hal.inria.fr/hal-01646064
28L. Straßburger.

Combinatorial Flows and their Normalisation, in: FSCD 2017 - 2nd International Conference on Formal Structures for Computation and Deduction, Oxford, United Kingdom, Leibniz International Proceedings in Informatics (LIPIcs), September 2017, vol. 84, pp. 311 - 3117. [ DOI : 10.4230/LIPIcs.FSCD.2017.31 ]

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

National Conferences with Proceedings

29G. Barany, G. Scherer.

Génération aléatoire de programmes guidée par la vivacité, in: JFLA: Journées Francophones des Langages Applicatifs, Banyuls-sur-Mer, France, January 2018.

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

Conferences without Proceedings

30B. Accattoli, B. Barras.

Environments and the Complexity of Abstract Machines, in: The 19th International Symposium on Principles and Practice of Declarative Programming, Namur, Belgium, October 2017. [ DOI : 10.1145/3131851.3131855 ]

https://hal.archives-ouvertes.fr/hal-01675358
31B. Accattoli, B. Barras.

The Negligible and Yet Subtle Cost of Pattern Matching, in: Programming Languages and Systems - 15th Asian Symposium, Suzhou, China, November 2017.

https://hal.archives-ouvertes.fr/hal-01675369
32B. Accattoli, G. Guerrieri.

Implementing Open Call-by-Value, in: Fundamentals of Software Engineering - 7th International Conference, Teheran, Iran, April 2017.

https://hal.archives-ouvertes.fr/hal-01675365
33D. Miller.

Using linear logic and proof theory to unify computational logic, in: Proceedings of Trends in Linear Logic and Applications (TLLA 17), Oxford, United Kingdom, September 2017.

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

Books or Proceedings Editing

34D. Miller (editor)

2nd International Conference on Formal Structures for Computation and Deduction (FSCD 2017), Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik, Oxford, United Kingdom, September 2017.

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

Internal Reports

35S. Marin, L. Straßburger.

On the Proof Theory of Indexed Nested Sequents for Classical and Intuitionistic Modal Logics, Inria, April 2017, n^o RR-9061.

https://hal.inria.fr/hal-01515797
36L. Straßburger, R. Kuznets.

Maehara-style Modal Nested Calculi, Inria Saclay, November 2017, n^o RR-9123.

https://hal.inria.fr/hal-01644750
37L. Straßburger.

Combinatorial Flows and Proof Compression, Inria Saclay, March 2017, n^o RR-9048.

https://hal.inria.fr/hal-01498468
38L. Straßburger.

Deep Inference, Expansion Trees, and Proof Graphs for Second Order Propositional Multiplicative Linear Logic, Inria Saclay Ile de France, May 2017, n^o RR-9071, 38 p.

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

Other Publications

39J. Courtiel, K. Yeats, N. Zeilberger.

Connected chord diagrams and bridgeless maps, November 2017, working paper or preprint.

https://hal.archives-ouvertes.fr/hal-01650141
40R. Kuznets, S. Marin, L. Straßburger.

Justification logic for constructive modal logic *, July 2017, IMLA 2017 - 7th Workshop on Intuitionistic Modal Logic and Applications.

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

References in notes

41J. A. Robinson, A. Voronkov (editors)

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

Computational Interpretations of Linear Logic, in: Theoretical Computer Science, 1993, vol. 111, pp. 3–57.
43B. 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
44J.-M. Andreoli.

Logic Programming with Focusing Proofs in Linear Logic, in: Journal of Logic and Computation, 1992, vol. 2, n^o 3, pp. 297–347.
45S. N. Artemov.

Operational modal logic, Cornell University, 1995, n^o MSI 95–29.
46A. Assaf, G. Burel, R. Cauderlier, D. Delahaye, G. Dowek, C. Dubois, F. Gilbert, P. Halmagrand, O. Hermant, R. Saillard.

Dedukti: a Logical Framework based on the $λ Π$ -Calculus Modulo Theory, 2016, Unpublished.

http://www.lsv.ens-cachan.fr/~dowek/Publi/expressing.pdf
47D. 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, pp. 278–292. [ DOI : 10.1007/978-3-642-14203-1 ]

http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/ijcar10.pdf
48G. 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
49M. P. Bonacina, S. Graham-Lengrand, N. Shankar.

A model-constructing framework for theory combination, Universita degli Studi di Verona, September 2016, n^o RR-99/2016.

https://hal.inria.fr/hal-01425305
50K. 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
51K. 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
52K. 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
53Z. Chihani, D. Miller, F. Renaud.

Checking Foundational Proof Certificates for First-Order Logic (extended abstract), in: Third International Workshop on Proof Exchange for Theorem Proving (PxTP 2013), J. C. Blanchette, J. Urban (editors), EPiC Series, EasyChair, 2013, vol. 14, pp. 58–66.
54Z. Chihani, D. Miller, F. Renaud.

Foundational proof certificates in first-order logic, in: CADE 24: Conference on Automated Deduction 2013, M. P. Bonacina (editor), Lecture Notes in Artificial Intelligence, 2013, n^o 7898, pp. 162–177.
55C. 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://www.easychair.org/publications/?page=2135488790
56P. Fontaine, J.-Y. Marion, S. Merz, L. P. Nieto, A. Tiu.

Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants, in: TACAS: Tools and Algorithms for the Construction and Analysis of Systems, 12th International Conference, H. Hermanns, J. Palsberg (editors), LNCS, Springer, 2006, vol. 3920, pp. 167–181.

http://dx.doi.org/10.1007/11691372_11
57A. 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
58J.-Y. Girard.

Linear Logic, in: Theoretical Computer Science, 1987, vol. 50, pp. 1–102.
59S. 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, n^o 1.

http://www.lix.polytechnique.fr/~lengrand/Work/Reports/TTSC09.pdf
60S. 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
61A. Guglielmi.

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

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

http://arxiv.org/abs/0709.1205
63A. 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.
64Q. Heath, D. Miller.

A framework for proof certificates in finite state exploration, in: Proceedings of the Fourth Workshop on Proof eXchange for Theorem Proving, C. Kaliszyk, A. Paskevich (editors), Electronic Proceedings in Theoretical Computer Science, Open Publishing Association, August 2015, n^o 186, pp. 11–26. [ DOI : 10.4204/EPTCS.186.4 ]

http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/pxtp2015.pdf
65D. Hughes.

Proofs Without Syntax, in: Annals of Mathematics, 2006, vol. 164, n^o 3, pp. 1065–1076.
66D. 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
67F. 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.
68C. Liang, D. Miller.

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

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

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

http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/lku.pdf
70P. 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.
71R. 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, pp. 80–136.

http://www.lix.polytechnique.fr/Labo/Dale.Miller/papers/mcdowell01.pdf
72R. 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.
73D. Miller.

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

Programming with Higher-Order Logic, Cambridge University Press, June 2012.

http://dx.doi.org/10.1017/CBO9781139021326
75D. 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.
76D. 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
77R. 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.
78G. Nelson, D. C. Oppen.

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

http://dx.doi.org/10.1145/357073.357079
79F. 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, pp. 202–206.
80B. 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, pp. 15–21.
81E. P. Robinson.

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

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

http://dx.doi.org/10.1145/2422.322411
83L. Straßburger, R. Kuznets.

Maehara-style Modal Nested Calculi, Inria Saclay, November 2017, n^o RR-9123.

https://hal.inria.fr/hal-01644750
84The Coq Development Team.

The Coq Proof Assistant Version 8.3 Reference Manual, Inria, October 2010.
85A. 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
86L. M. de Moura, D. Jovanovic.

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
87L. 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 |

Home