| [1] | Beniamino Accattoli. Proof nets and the call-by-value λ-calculus. Journal of Theoretical Computer Science (TCS), 2015. [ bib | DOI | http | http ] |
| [2] | Beniamino Accattoli, Pablo Barenbaum, and Damiano Mazza. A Strong Distillery. In Programming Languages and Systems - 13th Asian Symposium, APLAS 2015, volume 9458 of Lecture notes in computer science, pages 231--250, Pohang, South Korea, November 2015. [ bib | DOI | http | http ] |
| [3] | Beniamino Accattoli and Claudio Sacerdoti Coen. On the Relative Usefulness of Fireballs. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 2015. [ bib | DOI | http | http ] |
| [4] | Matthias Baaz, Alexander Leitsch, and Giselle Reis. A note on the complexity of classical and intuitionistic proofs. In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 657--666, 2015. [ bib | DOI | http ] |
| [5] | The Bedwyr system, 2015. Available at http://slimmer.gforge.inria.fr/bedwyr/. [ bib ] |
| [6] | Roberto Blanco and Dale Miller. Proof outlines as proof certificates: a system description. In Iliano Cervesato and Carsten Schürmann, editors, Proceedings First International Workshop on Focusing, volume 197 of Electronic Proceedings in Theoretical Computer Science, pages 7--14. Open Publishing Association, November 2015. [ bib | DOI | .html ] |
| [7] | Taus Brock-Nannestad and Kaustuv Chaudhuri. Disproving using the inverse method by iterated refinement of finite approximations. In Hans de Nivelle, editor, Proceedings of the 24th Automated Reasoning with Analytic Tableaux and Related Methods (TABLEAUX), volume 9323 of LNAI, pages 153--168, Wroclaw, Poland, September 2015. Springer. [ bib | DOI | .pdf ] |
| [8] | Taus Brock-Nannestad and Nicolas Guenot. Cut elimination in multifocused linear logic. In Sandra Alves and Iliano Cervesato, editors, Proceedings Third International Workshop on Linearity, LINEARITY 2014, Vienna, Austria, 13th July, 2014., volume 176 of EPTCS, pages 24--33, 2015. [ bib | DOI | http ] |
| [9] | Taus Brock-Nannestad and Nicolas Guenot. Focused linear logic and the λ-calculus. In Proceedings of the Thirty-first Conference on the Mathematical Foundations of Programming Semantics, Nijmegen, The Netherlands, June 22--25, 2015, pages 314--329, 2015. [ bib ] |
| [10] | Taus Brock-Nannestad, Nicolas Guenot, and Daniel Gustafsson. Computation in focused intuitionistic logic. In Moreno Falaschi and Elvira Albert, editors, Proceedings of the 17th International Symposium on Principles and Practice of Declarative Programming, Siena, Italy, July 14--16, 2015, pages 43--54, 2015. [ bib | DOI | http ] |
| [11] | Kaustuv Chaudhuri, Matteo Cimini, and Dale Miller. A lightweight formalization of the metatheory of bisimulation-up-to. In Xavier Leroy and Alwen Tiu, editors, Proceedings of the 4th ACM-SIGPLAN Conference on Certified Programs and Proofs, pages 157--166, Mumbai, India, January 2015. ACM. [ bib | DOI | http ] |
| [12] | Kaustuv Chaudhuri and Giselle Reis. An adequate compositional encoding of bigraph structure in linear logic with subexponentials. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), volume 9450 of LNCS, pages 146--161. Springer, November 2015. [ bib | DOI | .pdf ] |
| [13] | Zakaria Chihani. Certification of First-order proofs in classical and intuitionistic logics. PhD thesis, Ecole Polytechnique, August 2015. [ bib ] |
| [14] | Quentin Heath and Dale Miller. A framework for proof certificates in finite state exploration. In Cezary Kaliszyk and Andrei Paskevich, editors, Proceedings of the Fourth Workshop on Proof eXchange for Theorem Proving, number 186 in Electronic Proceedings in Theoretical Computer Science, pages 11--26. Open Publishing Association, August 2015. [ bib | DOI | .pdf ] |
| [15] | Alexander Leitsch, Giselle Reis, and Bruno Woltzenlogel Paleo. Epsilon terms in intuitionistic sequent calculus. 2015. Hilbert's Epsilon and Tau in Logic, Informatics and Linguistics Workshop. [ bib ] |
| [16] | Chuck Liang and Dale Miller. On subexponentials, synthetic connectives, and multi-level delimited control. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), number 9450 in LNCS, November 2015. [ bib | DOI | .pdf ] |
| [17] | Tomer Libal. Regular patterns in second-order unification. In Automated Deduction - CADE-25 - 25th International Conference on Automated Deduction, Berlin, Germany, August 1-7, 2015, Proceedings, pages 557--571, 2015. [ bib ] |
| [18] | Dale Miller. Foundational proof certificates. In David Delahaye and Bruno Woltzenlogel Paleo, editors, All about Proofs, Proofs for All, volume 55 of Mathematical Logic and Foundations, pages 150--163. College Publications, London, UK, January 2015. [ bib | .pdf ] |
| [19] | Dale Miller. Proof checking and logic programming. In Moreno Falaschi, editor, Logic-Based Program Synthesis and Transformation (LOPSTR) 2015, number 9527 in LNCS, pages 3--17. Springer, 2015. [ bib | DOI ] |
| [20] | Dale Miller. Proof checking and logic programming. In Elvira Albert, editor, ACM SIGPLAN Conference on Principles and Practice of Declarative Programming (PPDP), page 18. ACM, July 2015. [ bib | DOI ] |
| [21] | Dale Miller and Marco Volpe. Focused labeled proof systems for modal logic. In Martin Davis, Ansgar Fehnker, Annabelle McIver, and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), number 9450 in LNCS, pages 266--280, November 2015. [ bib | DOI ] |
| [22] | Giselle Reis. Importing SMT and connection proofs as expansion trees. 2015. Proof Exchange for Theorem Proving (PxTP). [ bib | http ] |
| [23] | Damien Rouhling, Mahfuza Farooque, Stéphane Graham-Lengrand, Assia Mahboubi, and Jean-Marc Notin. Axiomatic constraint systems for proof search modulo theories. In Carsten Lutz and Silvio Ranise, editors, Proceedings of the 9th International Symposium on Frontiers of Combining Systems (FroCoS'15), Lecture Notes in Computer Science. Springer-Verlag, September 2015. [ bib ] |
| [24] | Yuting Wang and Kaustuv Chaudhuri. A proof-theoretic characterization of independence in type theory. In Thorsten Altenkirch, editor, Proceedings of the 13th International Conference on Typed Lambda Calculi and Applications (TLCA), Leibniz International Proceedings in Informatics (LIPIcs), pages 332--346, Warsaw, Poland, July 2015. Schloss Dagstuhl--Leibniz-Zentrum für Informatik. [ bib | DOI | http ] |
This file was generated by bibtex2html 1.98.