All Slimmer related publications

  1. David Baelde. A linear approach to the proof-theory of least and greatest fixed points. PhD thesis, Ecole Polytechnique, December 2008. [ bib | http ]
  2. David Baelde. On the expressivity of minimal generic quantification. In A. Abel and C. Urban, editors, International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice (LFMTP 2008), number 228 in ENTCS, pages 3-19, 2008. [ bib | http ]
  3. 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 ]
  4. David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu. A User Guide to Bedwyr, November 2006. [ bib | .pdf ]
  5. David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu. The Bedwyr system for model checking over syntactic expressions. In F. Pfenning, editor, 21th Conf. on Automated Deduction (CADE), number 4603 in LNAI, pages 391-397. Springer, 2007. [ bib | .pdf ]
  6. 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 ]
  7. David Baelde and Dale Miller. Least and greatest fixed points in linear logic: extended version. Technical report, available from the first author's web page, April 2007. [ bib | .pdf ]
  8. 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 | .pdf ]
  9. 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 ]
  10. 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 ]
  11. 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 ENTCS, pages 85-100, 2008. [ bib | http | .pdf ]
  12. Andrew Gacek, Dale Miller, and Gopalan Nadathur. Nominal abstraction. Extended version of LICS 2008 paper. Accepted to Information and Computation, September 2010. [ bib | http ]
  13. Andrew Gacek, Dale Miller, and Gopalan Nadathur. A two-level logic approach to reasoning about computations. Accepted to the J. of Automated Reasoning, August 2010. [ bib | http ]
  14. Chuck Liang and Dale Miller. Focusing and polarization in intuitionistic logic. In J. Duparc and T. A. Henzinger, editors, CSL 2007: Computer Science Logic, volume 4646 of LNCS, pages 451-465. Springer, 2007. [ bib | .pdf ]
  15. Chuck Liang and Dale Miller. On focusing and polarities in linear logic and intuitionistic logic. Extended version of accepted paper., September 2007. [ bib | http | .pdf ]
  16. Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logics. Theoretical Computer Science, 410(46):4747-4768, 2009. [ bib | http ]
  17. Chuck Liang and Dale Miller. A unified sequent calculus for focused proofs. In LICS: 24th Symp. on Logic in Computer Science, pages 355-364, 2009. [ bib | .pdf ]
  18. Dale Miller. Representing and reasoning with operational semantics. In U. Furbach and N. Shankar, editors, Proceedings of IJCAR: International Joint Conference on Automated Reasoning, volume 4130 of LNAI, pages 4-20, August 2006. [ bib | .dvi | .pdf ]
  19. Dale Miller. Formalizing operational semantic specifications in logic. Concurrency Column of the Bulletin of the EATCS, October 2008. [ bib | .pdf ]
  20. Dale Miller. Formalizing operational semantic specifications in logic. In Proceedings of the 17th International Workshop on Functional and (Constraint) Logic Programming (WFLP 2008), volume 246, pages 147-165, August 2009. [ bib | http ]
  21. 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 ]
  22. Dale Miller and Vivek Nigam. Incorporating tables into proofs. In J. Duparc and T. A. Henzinger, editors, CSL 2007: Computer Science Logic, volume 4646 of LNCS, pages 466-480. Springer, 2007. [ bib | .pdf ]
  23. Dale Miller and Alexis Saurin. A game semantics for proof search: Preliminary results. In Proceedings of the Mathematical Foundations of Programming Semantics (MFPS05), number 155 in ENTCS, pages 543-563, 2006. [ bib | .pdf ]
  24. Dale Miller and Alexis Saurin. From proofs to focused proofs: a modular proof of focalization in linear logic. In J. Duparc and T. A. Henzinger, editors, CSL 2007: Computer Science Logic, volume 4646 of LNCS, pages 405-419. Springer, 2007. [ bib | .pdf ]
  25. Alberto Momigliano and Alwen Tiu. Induction and co-induction in sequent calculus. In Mario Coppo, Stefano Berardi, and Ferruccio Damiani, editors, Post-proceedings of TYPES 2003, number 3085 in LNCS, pages 293-308, January 2003. [ bib | .pdf ]
  26. Elaine Pimentel and Dale Miller. On the specification of sequent systems. In LPAR 2005: 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning, number 3835 in LNAI, pages 352-366, 2005. [ bib | .pdf ]
  27. Alexis Saurin. Separation with streams in the λμ-calculus. In 20th IEEE Symposium on Logic in Computer Science (LICS 2005), pages 356-365. IEEE Computer Society, 2005. [ bib ]
  28. 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 | http ]
  29. 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 ]