| [1] | Alexis Bernadet and Stéphane Graham-Lengrand. A big-step operational semantics via non-idempotent intersection types. Submitted, April 2013. [ bib ] |
| [2] | Alexis Bernadet and Stéphane Graham-Lengrand. Non-idempotent intersection types and strong normalisation. Logical Methods in Computer Science, 9(4), 2013. [ bib | DOI | http ] |
| [3] | Guillaume Burel. A shallow embedding of resolution and superposition proofs into the λΠ-calculus modulo. In J. C. Blanchette and J. Urban, editors, Third International Workshop on Proof Exchange for Theorem Proving (PxTP 2013), volume 14 of EPiC Series, pages 43--57. EasyChair, 2013. [ bib ] |
| [4] | Kaustuv Chaudhuri. Profound: a linking-based interactive prover, 2013. Available at: http://chaudhuri.info/software/profound/. [ bib ] |
| [5] | Kaustuv Chaudhuri. Subformula linking as an interaction method. In Sandrine Blazy, Christine Paulin-Mohring, and David Pichardie, editors, Proceedings of the 4th Conference on Interactive Theorem Proving (ITP), volume 7998 of LNCS, pages 386--401. Springer, July 2013. [ bib | .pdf ] |
| [6] | Kaustuv Chaudhuri, Denis Cousineau, Damien Doligez, Markus Kuppe, Leslie Lamport, Tomer Libal, Stephan Merz, and Hernán Vanzetto. TLAPS: the TLA+ proof system, 2013. Available from http://tla.msr-inria.inria.fr/tlaps/. [ bib ] |
| [7] | Kaustuv Chaudhuri and Joëlle Despeyroux. A hybrid linear logic for constrained transition systems. Collected Abstracts of the 19th Conference on Types for Proofs and Programs (TYPES), April 2013. [ bib | .pdf ] |
| [8] | Zakaria Chihani, Dale Miller, and Fabien Renaud. Checking foundational proof certificates for first-order logic (extended abstract). In J. C. Blanchette and J. Urban, editors, Third International Workshop on Proof Exchange for Theorem Proving (PxTP 2013), volume 14 of EPiC Series, pages 58--66. EasyChair, 2013. [ bib ] |
| [9] | Zakaria Chihani, Dale Miller, and Fabien Renaud. Foundational proof certificates in first-order logic. In Maria Paola Bonacina, editor, CADE 24: Conference on Automated Deduction 2013, number 7898 in LNAI, pages 162--177, 2013. [ bib | DOI ] |
| [10] | Mahfuza Farooque. Automated reasoning techniques in sequent calculus. Ph.d. thesis, Ecole Polytechnique, 2013. [ bib ] |
| [11] | Mahfuza Farooque and Stéphane Graham-Lengrand. Sequent calculi with procedure calls. Technical report, Laboratoire d'informatique de l'école polytechnique - LIX, CNRS-Ecole Polytechnique-INRIA, January 2013. [ bib | http ] |
| [12] | Mahfuza Farooque, Stéphane Graham-Lengrand, and Assia Mahboubi. A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus. In Alberto Momigliano, Brigitte Pientka, and Randy Pollack, editors, Proceedings of the 2013 ACM SIGPLAN Workshop on Logical Frameworks & Meta-Languages: Theory & Practice, LFMTP'13, pages 3--13. ACM, September 2013. [ bib | .pdf ] |
| [13] | Ivan Gazeau. Safe Programming in finite precision: Controling the errors and information leaks. Ph.d. thesis, Ecole Polytechnique, 2013. [ bib ] |
| [14] | Ivan Gazeau, Dale Miller, and Catuscia Palamidessi. Preserving differential privacy under finite-precision semantics. In Proceedings 11th International Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL), pages 1--18, 2013. [ bib | http ] |
| [15] | Stéphane Graham-Lengrand. Psyche: a proof-search engine based on sequent calculus with an LCF-style architecture. In Didier Galmiche and Dominique Larchey-Wendling, editors, International Conference on Automated Reasoning with Analytic Tableaux and Related Methods (Tableaux'13), volume 8123 of LNCS, pages 149--156. Springer, September 2013. [ bib ] |
| [16] | Stéphane Graham-Lengrand and Luca Paolini, editors. Proceedings Sixth Workshop on Intersection Types and Related Systems, ITRS 2013, Dubrovnik, Croatia, 29th June 2012, volume 121 of EPTCS, 2013. [ bib | DOI ] |
| [17] | Nicolas Guenot. Nested Deduction in Logical Foundations for Computation. Ph.d. thesis, Ecole Polytechnique, 2013. [ bib ] |
| [18] | François Lamarche. Path Functors in Cat. Technical Report hal-00831430, INRIA, April 2013. Submitted. [ bib | http | .pdf ] |
| [19] | Chuck Liang and Dale Miller. Kripke semantics and proof systems for combining intuitionistic logic and classical logic. Annals of Pure and Applied Logic, 164(2):86--111, February 2013. [ bib | DOI | http ] |
| [20] | Chuck Liang and Dale Miller. Unifying classical and intuitionistic logics for computational control. In Orna Kupferman, editor, 28th Symp. on Logic in Computer Science, pages 283--292, 2013. [ bib | .pdf ] |
| [21] | Dale Miller. Foundational proof certificates: Making proof universal and permanent. In Alberto Momigliano, Brigitte Pientka, and Randy Pollack, editors, Proceedings of the 2013 ACM SIGPLAN Workshop on Logical Frameworks & Meta-Languages: Theory & Practice, LFMTP'13, page 1. ACM, September 2013. [ bib | .pdf ] |
| [22] | Dale Miller and Elaine Pimentel. A formal framework for specifying sequent calculus proof systems. Theoretical Computer Science, 474:98--116, 2013. [ bib | DOI | http ] |
| [23] | Dale Miller and Alwen Tiu. Extracting proofs from tabled proof search. In Georges Gonthier and Michael Norrish, editors, Certified Programs and Proofs, number 8307 in LNCS, pages 194--210, Melburne, Australia, December 2013. Springer. [ bib | .pdf ] |
| [24] | Lutz Straßburger. Cut elimination in nested sequents for intuitionistic modal logics. In Frank Pfenning, editor, Foundations of Software Science and Computation Structures, 16th International Conference (FOSSACS), volume 7794 of LNCS, pages 209--224. Springer, 2013. [ bib | DOI ] |
| [25] | Yuting Wang, Kaustuv Chaudhuri, Andrew Gacek, and Gopalan Nadathur. Reasoning about higher-order relational specifications. In Tom Schrijvers, editor, Proceedings of the 15th International Symposium on Princples and Practice of Declarative Programming (PPDP), pages 157--168, Madrid, Spain, September 2013. [ bib | DOI | .pdf ] |
This file was generated by bibtex2html 1.98.