| [1] | David Baelde, Dale Miller, and Zachary Snow. Focused inductive theorem proving. In J. Giesl and R. Hähnle, editors, Fifth International Joint Conference on Automated Reasoning, number 6173 in LNCS, pages 278--292, 2010. [ bib | DOI | .pdf ] |
| [2] | Paola Bruscoli, Alessio Guglielmi, Tom Gundersen, and Michel Parigot. A quasipolynomial cut-elimination procedure in deep inference via atomic flows and threshold formulae. In Edmund Clarke and Andrei Voronkov, editors, Proceedings of the 16th International Conference on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR 2009), volume 6355 of LNAI, Dakar, Senegal, April 2010. Springer. [ bib | .pdf ] |
| [3] | Kaustuv Chaudhuri. Classical and intuitionistic subexponential logics are equally expressive. In Anuj Dawar and Helmut Veith, editors, CSL 2010: Computer Science Logic, volume 6247 of LNCS, pages 185--199, Brno, Czech Republic, August 2010. Springer. [ bib | DOI | http ] |
| [4] | Kaustuv Chaudhuri. Magically constraining the inverse method using dynamic polarity assignment. In Christian Fermüller and Andrei Voronkov, editors, Proc. 17th Int. Conf. on Logic for Programming, Artificial Intelligence, and Reasoning (LPAR), volume 6397 of LNCS, pages 202--216, Yogyakarta, Indonesia, October 2010. Springer. [ bib | DOI | http ] |
| [5] | Kaustuv Chaudhuri, Damien Doligez, Leslie Lamport, and Stephan Merz. Verifying safety properties with the TLA+ proof system. In Jürgen Giesl and Reiner Hähnle, editors, Fifth International Joint Conference on Automated Reasoning, volume 6173 of LNAI, pages 142--148, Edinburgh, UK, July 2010. Springer. [ bib | DOI | http ] |
| [6] | Kaustuv Chaudhuri, Damien Doligez, Stephan Merz, and Leslie Lamport. The TLA+ proof system: Building a heterogeneous verification platform. In Ana Cavalcanti, David Déharbe, Marie-Claude Gaudel, and Jim Woodcock, editors, Proceedings of the 7th International Colloquium on Theoretical Aspects of Computing (ICTAC), volume 6256 of LNCS, page 44, Natal, Rio Grande do Norte, Brazil, September 2010. Springer. [ bib | DOI | http ] |
| [7] | Olivier Delande, Dale Miller, and Alexis Saurin. Proof and refutation in MALL as a game. Annals of Pure and Applied Logic, 161(5):654--672, February 2010. [ bib | DOI | .pdf ] |
| [8] | Andrew Gacek. Relating nominal and higher-order abstract syntax specifications. In Proceedings of the 2010 Symposium on Principles and Practice of Declarative Programming, pages 177--186. ACM, July 2010. [ bib | .pdf ] |
| [9] | Nicolas Guenot. Focused proof search for linear logic in the calculus of structures. In Manuel V. Hermenegildo and Torsten Schaub, editors, Technical Communications of the 26th International Conference on Logic Programming (ICLP 2010), volume 7 of Leibniz International Proceedings in Informatics (LIPIcs), pages 84--93, Edinburgh, United Kingdom, July 2010. Schloss Dagstuhl--Leibniz-Zentrum für Informatik. [ bib | DOI | .pdf ] |
| [10] | Alessio Guglielmi, Tom Gundersen, and Michel Parigot. A proof calculus which reduces syntactic bureaucracy. In Christopher Lynch, editor, Proceedings of the 21st International Conference on Rewriting Techniques and Applications (RTA 2010), volume 6 of Leibniz International Proceedings in Informatics (LIPIcs), pages 135--150, Edinburgh, United Kingdom, July 2010. Schloss Dagstuhl--Leibniz-Zentrum für Informatik. [ bib | DOI | http ] |
| [11] | Alessio Guglielmi, Tom Gundersen, and Lutz Straßburger. Breaking paths in atomic flows for classical logic. In Jean-Pierre Jouannaud, editor, 25th Symp. on Logic in Computer Science, pages 284--293, Edinburgh, United Kingdom, July 2010. [ bib | DOI | .pdf ] |
| [12] | Dale Miller. Finding unity in computational logic. In Proceedings of the 2010 ACM-BCS Visions of Computer Science Conference, ACM-BCS '10, pages 3:1--3:13. British Computer Society, April 2010. [ bib | .pdf ] |
| [13] | Dale Miller. Reasoning about computations using two-levels of logic. In K. Ueda, editor, Proceedings of the 8th Asian Symposium on Programming Languages and Systems (APLAS'10), number 6461 in LNCS, pages 34--46, 2010. [ bib | .pdf ] |
| [14] | Vivek Nigam and Dale Miller. A framework for proof systems. J. of Automated Reasoning, 45(2):157--188, 2010. [ bib | http | .pdf ] |
| [15] | Alexis Saurin. Typing streams in Λμ-calculus. ACM Transactions on Computational Logic, 11(4), 2010. [ bib | .pdf ] |
| [16] | Lutz Straßburger. What is the problem with proof nets for classical logic? In Fernando Ferreira, Benedikt Löwe, Elvira Mayordomo, and Luís Mendes Gomes, editors, Programs, Proofs, Processes, 6th Conference on Computability in Europe (CiE 2010), volume 6158 of LNCS, pages 406--416, Ponta Delgada, Azores, Portugal, June 2010. Springer. [ bib | DOI | .pdf ] |
| [17] | Alwen Tiu and Dale Miller. Proof search specifications of bisimulation and modal logics for the π-calculus. ACM Trans. on Computational Logic, 11(2), 2010. [ bib | DOI | http ] |
This file was generated by bibtex2html 1.98.