| [1] | The Abella prover, 2012. Available at http://abella-prover.org/. [ bib ] |
| [2] | Beniamino Accattoli. An abstract factorization theorem for explicit substitutions. In Ashish Tiwari, editor, 23rd International Conference on Rewriting Techniques and Applications (RTA), volume 15 of Leibniz International Proceedings in Informatics (LIPIcs), pages 6--21. Schloss Dagstuhl--Leibniz-Zentrum für Informatik, 2012. [ bib | DOI ] |
| [3] | Beniamino Accattoli. Proof pearl: Abella formalization of lambda calculus cube property. In Chris Hawblitzel and Dale Miller, editors, Second International Conference on Certified Programs and Proofs, volume 7679 of LNCS, pages 173--187. Springer, 2012. [ bib ] |
| [4] | Beniamino Accattoli and Delia Kesner. The permutative λ-calculus. In Logic for Programming, Artificial Intelligence, and Reasoning - 18th International Conference (LPAR-18), volume 7180 of LNCS, pages 23--36. Springer, 2012. [ bib | DOI | http ] |
| [5] | Beniamino Accattoli and Delia Kesner. Preservation of strong normalisation modulo permutations for the structural lambda-calculus. Logical Methods in Computer Science, 8(1), 2012. [ bib | DOI | http ] |
| [6] | Beniamino Accattoli and Ugo Dal Lago. On the invariance of the unitary cost model for head reduction. In Ashish Tiwari, editor, 23rd International Conference on Rewriting Techniques and Applications (RTA), volume 15 of Leibniz International Proceedings in Informatics (LIPIcs), pages 22--37. Schloss Dagstuhl--Leibniz-Zentrum für Informatik, 2012. [ bib | DOI ] |
| [7] | Beniamino Accattoli and Luca Paolini. Call-by-value solvability, revisited. In Eleventh International Symposium on Functional and Logic Programming (FLOPS 2012), volume 7294 of LNCS, pages 4--16. Springer, 2012. [ bib | DOI ] |
| [8] | Kaustuv Chaudhuri. Compact proof certificates for linear logic. In Chris Hawblitzel and Dale Miller, editors, Proceedings of the Second Internatinal Conference on Certified Programs and Proofs (CPP), volume 7679 of LNCS, pages 208--223, Kyoto, Japan, December 2012. Springer. [ bib | DOI | .pdf ] |
| [9] | Kaustuv Chaudhuri, Stefan Hetzl, and Dale Miller. A systematic approach to canonicity in the classical sequent calculus. In Patrick Cégielski and Arnaud Durand, editors, CSL 2012: Computer Science Logic, volume 16 of Leibniz International Proceedings in Informatics (LIPIcs), pages 183--197. Schloss Dagstuhl--Leibniz-Zentrum für Informatik, September 2012. [ bib | DOI ] |
| [10] | Mahfuza Farooque, Stéphane Lengrand, and Assia Mahboubi. Simulating the DPLL(T) procedure in a sequent calculus with focusing. Technical report, Laboratoire d'informatique de l'école polytechnique - LIX, CNRS-Ecole Polytechnique-INRIA, March 2012. [ bib | http ] |
| [11] | Mahfuza Farooque, Stéphane Lengrand, and Assia Mahboubi. Two simulations about DPLL(T). Technical report, Laboratoire d'informatique de l'école polytechnique - LIX, CNRS-Ecole Polytechnique-INRIA, March 2012. [ bib | http ] |
| [12] | Andrew Gacek, Dale Miller, and Gopalan Nadathur. A two-level logic approach to reasoning about computations. J. of Automated Reasoning, 49(2):241--273, 2012. [ bib | DOI | http ] |
| [13] | Ivan Gazeau, Dale Miller, and Catuscia Palamidessi. A non-local method for robustness analysis of floating point programs. In Herbert Wiklicky and Mieke Massink, editors, Proceedings of the 10th Workshop on Quantitative Aspects of Programming Languages and Systems (QAPL 2012), volume 85 of Electronic Proceedings in Theoretical Computer Science, pages 63--76, 2012. [ bib | DOI ] |
| [14] | Bernhard Gramlich, Dale Miller, and Uli Sattler, editors. Automated Reasoning: 6th International Joint Conference, IJCAR 2012, Manchester, UK, June 2012, Proceedings, volume 7364 of LNAI. Springer, 2012. [ bib | DOI ] |
| [15] | Chris Hawblitzel and Dale Miller, editors. CPP: Second International Conference on Certified Programs and Proofs, volume 7679 of LNCS. Springer, 2012. [ bib | DOI ] |
| [16] | Stefan Hetzl. Project Presentation: Algorithmic Structuring and Compression of Proofs (ASCOP). In J. Jeuring et al., editor, Conference on Intelligent Computer Mathematics (CICM) 2012, volume 7362 of Lecture Notes in Artificial Intelligence, pages 437--441. Springer, 2012. [ bib ] |
| [17] | Stefan Hetzl and Lutz Straßburger. Herbrand-Confluence for Cut-Elimination in Classical First-Order Logic. In Patrick Cégielski and Arnaud Durand, editors, Computer Science Logic (CSL) 2012, volume 16 of Leibniz International Proceedings in Informatics (LIPIcs), pages 320--334. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 2012. [ bib ] |
| [18] | François Lamarche. Modelling Martin Löf Type Theory in Categories. In Ch. Retoré and J. Gilibert, editors, Logic, Categories, Semantics, special issue of J. of Applied Logic, Bordeaux, France, June 2012. Ch. Retoré and J. Gilibert, Elsevier North-Holland. Scheduled to appear in June 2013. [ bib | http | .pdf ] |
| [19] | Dale Miller and Zoltán Ésik, editors. Proceedings 8th Workshop on Fixed Points in Computer Science, volume 77 of Electronic Proceedings in Theoretical Computer Science, 2012. [ bib | DOI | .pdf ] |
| [20] | Dale Miller and Gopalan Nadathur. Programming with Higher-Order Logic. Cambridge University Press, June 2012. [ bib | DOI ] |
| [21] | Psyche: the Proof-Search factorY for Collaborative HEuristics, 2012. Available at http://www.lix.polytechnique.fr/~lengrand/Psyche. [ bib ] |
| [22] | Lutz Straßburger. Extension without cut. Annals of Pure and Applied Logic, 163(12):1995--2007, 2012. [ bib | DOI | http | .pdf ] |
This file was generated by bibtex2html 1.98.