| [1] | David Baelde. On the proof theory of regular fixed points. In Martin Giese and Arild Waller, editors, TABLEAUX 09: Automated Reasoning with Analytic Tableaux and Related Methods, number 5607 in LNAI, pages 93-107, 2009. [ bib | .pdf ] |
| [2] | David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu. A User Guide to Bedwyr, November 2006. [ bib | .pdf ] |
| [3] | David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu. The Bedwyr system for model checking over syntactic expressions. In Frank Pfenning, editor, 21th Conference on Automated Deduction (CADE), number 4603 in LNAI, pages 391-397. Springer, 2007. [ bib | .pdf ] |
| [4] | David Baelde and Dale Miller. Least and greatest fixed points in linear logic. In N. Dershowitz and A. Voronkov, editors, International Conference on Logic for Programming and Automated Reasoning (LPAR), volume 4790 of LNCS, pages 92-106, 2007. [ bib | .pdf ] |
| [5] | Andrew Gacek. The Abella interactive theorem prover (system description). In Alessandro Armando, Peter Baumgartner, and Gilles Dowek, editors, Fourth International Joint Conference on Automated Reasoning, volume 5195 of LNCS, pages 154-161. Springer, 2008. [ bib | http ] |
| [6] | Andrew Gacek, Dale Miller, and Gopalan Nadathur. Combining generic judgments with recursive definitions. In F. Pfenning, editor, 23th Symp. on Logic in Computer Science, pages 33-44. IEEE Computer Society Press, 2008. [ bib | .pdf ] |
| [7] | Andrew Gacek, Dale Miller, and Gopalan Nadathur. Reasoning in Abella about structural operational semantics specifications. In A. Abel and C. Urban, editors, International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008), number 228 in Electronic Notes in Theoretical Computer Science, pages 85-100, 2008. [ bib | http | .pdf ] |
| [8] | Raymond McDowell and Dale Miller. Reasoning with higher-order abstract syntax in a logical framework. ACM Trans. on Computational Logic, 3(1):80-136, 2002. [ bib | .pdf ] |
| [9] | Gopalan Nadathur and Natalie Linnell. Practical higher-order pattern unification with on-the-fly raising. In ICLP 2005: 21st International Logic Programming Conference, volume 3668 of LNCS, pages 371-386, Sitges, Spain, October 2005. Springer. [ bib ] |
| [10] | Gopalan Nadathur and Xiaochu Qi. Optimizing the runtime processing of types in polymorphic logic programming languages. In Geoff Sutcliffe and Andrei Voronkov, editors, Logic for Programming, Artificial Intelligence, and Reasoning, 12th International Conference, LPAR 2005, Montego Bay, Jamaica, December 2-6, 2005, Proceedings, volume 3835 of LNCS, pages 110-124. Springer, 2005. [ bib ] |
| [11] | Alwen Tiu. A Logical Framework for Reasoning about Logical Specifications. PhD thesis, Pennsylvania State University, May 2004. [ bib | http | .pdf ] |
| [12] | Alwen Tiu, Gopalan Nadathur, and Dale Miller. Mixing finite success and finite failure in an automated prover. In Empirically Successful Automated Reasoning in Higher-Order Logics (ESHOL'05), pages 79-98, December 2005. [ bib | .pdf ] |
This file was generated by bibtex2html 1.94.