Bibliography by First Author

[ACMP84] Peter B. Andrews, Eve Longini Cohen, Dale Miller, and Frank Pfenning. Automating higher order logic. In Automated Theorem Proving: After 25 Years, pages 169-192. American Mathematical Society, Providence, RI, 1984. [ bib ]
[BGM+06] David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and Alwen Tiu. A User Guide to Bedwyr, November 2006. [ bib | .pdf ]
[BGM+07] 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 ]
[BM07a] 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 ]
[BM07b] 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 ]
[CMS08] Kaustuv Chaudhuri, Dale Miller, and Alexis Saurin. Canonical sequent proofs via multi-focusing. In Giorgio Ausiello, Juhani Karhumäki, Giancarlo Mauri, and Luke Ong, editors, Fifth IFIP International Conference on Theoretical Computer Science, volume 273 of IFIP International Federation for Information Processing, pages 383-396. Boston: Springer, September 2008. [ bib | .pdf ]
[DM06] Roberto DiCosmo and Dale Miller. Linear logic. In Edward N. Zalta, editor, The Stanford Encyclopedia of Philosophy. Stanford University, 2006. [ bib | http ]
[DM08a] Olivier Delande and Dale Miller. A neutral approach to proof and refutation in MALL. In F. Pfenning, editor, 23th Symp. on Logic in Computer Science, pages 498-508. IEEE Computer Society Press, 2008. [ bib | .pdf ]
[DM08b] Olivier Delande and Dale Miller. A neutral approach to proof and refutation in MALL: extended report. Available via the authors web pages, 2008. [ bib ]
[DMS08] Olivier Delande, Dale Miller, and Alexis Saurin. Proof and refutation in MALL as a game. Submitted for publication, October 2008. [ bib ]
[FM87] Amy Felty and Dale Miller. Proof explanation and revision. Draft, 1987. [ bib ]
[FM88] Amy Felty and Dale Miller. Specifying theorem provers in a higher-order logic programming language. In Ninth International Conference on Automated Deduction, pages 61-80, Argonne, IL, May 1988. Springer-Verlag. [ bib ]
[FM89] Amy Felty and Dale Miller. A meta language for type checking and inference: An extended abstract. Presented at the 1989 Workshop on Programming Logic, Bålstad, Sweden, 1989. [ bib ]
[FM90] Amy Felty and Dale Miller. Encoding a dependent-type λ-calculus in a logic programming language. In Mark Stickel, editor, Proceedings of the 1990 Conference on Automated Deduction, volume 449 of LNAI, pages 221-235. Springer, 1990. [ bib ]
[GMN08a] 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 ]
[GMN08b] Andrew Gacek, Dale Miller, and Gopalan Nadathur. Reasoning in Abella about structural operational semantics specifications. In A. Abel and C. Urban, editors, LFMTP 2008: International Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, pages 75-89, 2008. [ bib | .pdf ]
[HM88] John Hannan and Dale Miller. Uses of higher-order unification for implementing program transformers. In Fifth International Logic Programming Conference, pages 942-959, Seattle, Washington, August 1988. MIT Press. [ bib ]
[HM89a] John Hannan and Dale Miller. Deriving mixed evaluation from standard evaluation for a simple functional programming language. In Jan L. A. van de Snepscheut, editor, 1989 International Conference on Mathematics of Program Construction, volume 375 of LNCS, pages 239-255. Springer-Verlag, 1989. UPenn CIS Tech Report MS-CIS-89-28. [ bib | .pdf ]
[HM89b] John Hannan and Dale Miller. A meta-logic for functional programming. In H. Abramson and M. Rogers, editors, Meta-Programming in Logic Programming, chapter 24, pages 453-476. MIT Press, 1989. [ bib ]
[HM90a] John Hannan and Dale Miller. From operational semantics to abstract machines: Preliminary results. In M. Wand, editor, Proceedings of the 1990 ACM Conference on Lisp and Functional Programming, pages 323-332. ACM, ACM Press, 1990. [ bib ]
[HM90b] Joshua Hodas and Dale Miller. Representing objects in a logic programming language with scoping constructs. In David H. D. Warren and Peter Szeredi, editors, 1990 International Conference in Logic Programming, pages 511-526. MIT Press, June 1990. [ bib ]
[HM91] Joshua Hodas and Dale Miller. Logic programming in a fragment of intuitionistic linear logic: Extended abstract. In G. Kahn, editor, Sixth Annual Symposium on Logic in Computer Science, pages 32-42, Amsterdam, July 1991. [ bib ]
[HM92] John Hannan and Dale Miller. From operational semantics to abstract machines. Mathematical Structures in Computer Science, 2(4):415-459, 1992. [ bib ]
[HM94] Joshua Hodas and Dale Miller. Logic programming in a fragment of intuitionistic linear logic. Information and Computation, 110(2):327-365, 1994. [ bib ]
[LAB+06] Gary T. Leavens, Jean-Raymond Abrial, Don Batory, Michael Butler, Alessandro Coglio, Kathi Fisler, Eric Hehner, Cliff Jones, Dale Miller, Simon Peyton-Jones, Murali Sitaraman, Douglas R. Smith, and Aaron Stump. Roadmap for enhanced languages and methods to aid verification. In Fifth International Conference on Generative Programming and Component Engineering (GPCE), pages 221-235. ACM, October 2006. [ bib ]
[LM07a] 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. Extended version to appear in TCS. [ bib | .pdf ]
[LM07b] Chuck Liang and Dale Miller. On focusing and polarities in linear logic and intuitionistic logic. September 2007. [ bib | http | .pdf ]
[LM08] Chuck Liang and Dale Miller. Focusing and polarization in linear, intuitionistic, and classical logics. Accepted to Theoretical Computer Science, 2008. [ bib ]
[MCA82] Dale A. Miller, Eve Longini Cohen, and Peter B. Andrews. A look at TPS. In Donald W. Loveland, editor, Sixth Conference on Automated Deduction, volume 138 of LNCS, pages 50-69, New York, 1982. Springer-Verlag. [ bib ]
[MF86] Dale Miller and Amy Felty. An integration of resolution and natural deduction theorem proving. In National Conference on Artificial Intelligence (AAAI-86), pages 198-202, Philadelphia, PA, August 1986. [ bib ]
[Mil83] Dale A. Miller. Proofs in Higher-order Logic. PhD thesis, Carnegie-Mellon University, August 1983. [ bib | .pdf ]
[Mil84] Dale A. Miller. Expansion tree proofs and their conversion to natural deduction proofs. In R. E. Shostak, editor, Seventh Conference on Automated Deduction, volume 170 of LNCS, pages 375-393, Napa CA, May 1984. Springer-Verlag. [ bib ]
[Mil86] Dale Miller. A theory of modules for logic programming. In Robert M. Keller, editor, Third Annual IEEE Symposium on Logic Programming, pages 106-114, Salt Lake City, Utah, September 1986. [ bib ]
[Mil87a] Dale Miller. Hereditary harrop formulas and logic programming. In Proceedings of the VIII International Congress of Logic, Methodology, and Philosophy of Science, pages 153-156, Moscow, August 1987. [ bib ]
[Mil87b] Dale A. Miller. A compact representation of proofs. Studia Logica, 46(4):347-370, 1987. [ bib ]
[Mil88] Dale Miller. Logic programming based on higher-order hereditary harrop formulas. Technical Report MS-CIS-88-77, Computer Science Department, University of Pennsylvania, September 1988. Transparencies for lectures at the Advanced School on Foundations of Logic Programming, Algehro, Sardinia. [ bib ]
[Mil89a] Dale Miller. Lexical scoping as universal quantification. In Sixth International Logic Programming Conference, pages 268-283, Lisbon, Portugal, June 1989. MIT Press. [ bib | .pdf ]
[Mil89b] Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification: Extended abstract. In Graham M. Birtwistle, editor, Proceedings of the 1989 Banff meeting on “Higher-Orders”, Banff, Canada, September 1989. [ bib ]
[Mil89c] Dale Miller. A logical analysis of modules in logic programming. Journal of Logic Programming, 6(1-2):79-108, January 1989. [ bib ]
[Mil90a] Dale Miller. Abstractions in logic programming. In Piergiorgio Odifreddi, editor, Logic and Computer Science, pages 329-359. Academic Press, 1990. [ bib | .pdf ]
[Mil90b] Dale Miller. An extension to ML to handle bound variables in data structures: Preliminary report. In Informal Proceedings of the Logical Frameworks BRA Workshop, Nice, France, June 1990. Available as UPenn CIS technical report MS-CIS-90-59. [ bib | .pdf ]
[Mil90c] Dale Miller. Semantics of a simple meta-logic. Unpublished draft, March 1990. [ bib ]
[Mil91a] Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. In Peter Schroeder-Heister, editor, Extensions of Logic Programming: International Workshop, Tübingen, volume 475 of LNAI, pages 253-281. Springer-Verlag, 1991. [ bib ]
[Mil91b] Dale Miller. A logic programming language with lambda-abstraction, function variables, and simple unification. J. of Logic and Computation, 1(4):497-536, 1991. [ bib ]
[Mil91c] Dale Miller. Proof theory as an alternative to model theory. Newsletter of the Association for Logic Programming, August 1991. Guest editorial. [ bib | .html ]
[Mil91d] Dale Miller. Unification of simply typed lambda-terms as logic programming. In Eighth International Logic Programming Conference, pages 255-269, Paris, France, June 1991. MIT Press. [ bib ]
[Mil92a] Dale Miller. Abstract syntax and logic programming. In Logic Programming: Proceedings of the First and Second Russian Conferences on Logic Programming, number 592 in LNAI, pages 322-337. Springer-Verlag, 1992. [ bib ]
[Mil92b] Dale Miller. Linear logic and logic programming: An overview. In Dale Miller, editor, Proceedings of the Workshop on Linear Logic and Logic Programming (Washington, DC), November 1992. Available as UPenn CIS technical report MS-CIS-92-80 and electronically from ftp.cis.upenn.edu in pub/meetings/LL+LP-proceedings. [ bib ]
[Mil92c] Dale Miller. A proposal for modules for λProlog: Preliminary draft. In Dale Miller, editor, Proceedings of the 1992 λProlog Workshop, 1992. [ bib ]
[Mil92d] Dale Miller. Unification under a mixed prefix. Journal of Symbolic Computation, 14(4):321-358, 1992. [ bib | .pdf ]
[Mil93] Dale Miller. The π-calculus as a theory in linear logic: Preliminary results. In E. Lamma and P. Mello, editors, 3rd Workshop on Extensions to Logic Programming, number 660 in LNCS, pages 242-265, Bologna, Italy, 1993. Springer-Verlag. [ bib | .pdf ]
[Mil94a] Dale Miller. A multiple-conclusion meta-logic. In S. Abramsky, editor, Ninth Annual Symposium on Logic in Computer Science, pages 272-281, Paris, July 1994. IEEE Computer Society Press. [ bib ]
[Mil94b] Dale Miller. A proposal for modules in λProlog. In R. Dyckhoff, editor, 4th Workshop on Extensions to Logic Programming, number 798 in LNCS, pages 206-221. Springer-Verlag, 1994. [ bib ]
[Mil95a] Dale Miller. Observations about using logic as a specification language. In M. Sessa, editor, Proceedings of GULP-PRODE'95: Joint Conference on Declarative Programming, Marina di Vietri (Salerno-Italy), September 1995. [ bib ]
[Mil95b] Dale Miller. A survey of linear logic programming. Computational Logic: The Newsletter of the European Network in Computational Logic, 2(2):63-67, December 1995. [ bib ]
[Mil96] Dale Miller. Forum: A multiple-conclusion specification logic. Theoretical Computer Science, 165(1):201-232, September 1996. [ bib ]
[Mil97] Dale Miller. Logic programming and meta-logic. In Helmut Schwichtenberg, editor, Logic of Computation, volume 157 of Nato ASI Series, pages 265-308. Springer, 1997. [ bib ]
[Mil98] Dale Miller. λProlog: an introduction to the language and its logic. Incomplete draft., 1998. [ bib | .pdf ]
[Mil99] Dale Miller. Sequent calculus and the specification of computation. In Ulrich Berger and Helmut Schwichtenberg, editors, Computational Logic, volume 165 of Nato ASI Series, pages 399-444. Springer, 1999. [ bib ]
[Mil00] Dale Miller. Abstract syntax for variable binders: An overview. In John Lloyd and et. al., editors, Computational Logic - CL 2000, number 1861 in LNAI, pages 239-253. Springer, 2000. [ bib | .pdf ]
[Mil01] Dale Miller. Encoding generic judgments: Preliminary results. In R. L. Crole S. J. Ambler and A. Momigliano, editors, ENTCS, volume 58. Elsevier Science Publishers, 2001. Proceedings of the MERLIN 2001 Workshop, Siena. [ bib ]
[Mil02a] Dale Miller. Higher-order quantification and proof search. In Hélène Kirchner and Christophe Ringeissen, editors, Proceedings of AMAST 2002, number 2422 in LNCS, pages 60-74, 2002. [ bib | .pdf ]
[Mil02b] Dale Miller. Higher-order quantification and proof search: an extended abstract, July 2002. Presented at Linear Logic 2002, FLoC, Copenhagen. [ bib ]
[Mil03a] Dale Miller. Definitions, unification, and the sequent calculus. In J. Levy, M. Kohlhase, J. Niehren, and M. Villaret, editors, Proceedings of the 17th International Workshop on Unification, UNIF'03, Technical Report DSIC-II/12/03, pages 1-2. Departamento de Sistemas Informàtics i Computació Universidad Politècnica de València, June 2003. Invited talk. [ bib ]
[Mil03b] Dale Miller. Encryption as an abstract data type. In Ruy de Queiroz, Elaine Pimentel, and Lucilia Figueiredo, editors, WoLLIC'2003, 10th Workshop on Logic, Language, Information and Computation, volume 84 of Electronic Notes in Theoretical Computer Science. Elsevier, 2003. Invited talk. [ bib ]
[Mil03c] Dale Miller. Encryption as an abstract data-type: An extended abstract. In Iliano Cervesato, editor, Proceedings of FCS'03: Foundations of Computer Security, pages 3-14, 2003. [ bib | .dvi | .ps | .pdf ]
[Mil03d] Dale Miller. Reasoning about proof search specifications: An abstract. In Theorem Proving in Higher Order Logics: 16th International Conference, TPHOLs 2003, volume 2758 of LNCS, page 204. Springer-Verlag, 2003. Invited speaker. [ bib | .dvi | .pdf ]
[Mil04a] Dale Miller. Bindings, mobility of bindings, and the -quantifier. In Jerzy Marcinkowski and Andrzej Tarlecki, editors, 18th International Workshop CSL 2004, volume 3210 of LNCS, page 24, 2004. [ bib | .pdf ]
[Mil04b] Dale Miller. Overview of linear logic programming. In Thomas Ehrhard, Jean-Yves Girard, Paul Ruet, and Phil Scott, editors, Linear Logic in Computer Science, volume 316 of London Mathematical Society Lecture Note, pages 119-150. Cambridge University Press, 2004. [ bib | .dvi | .ps | .pdf ]
[Mil06a] Dale Miller. Collection analysis for Horn clause programs. In Proceedings of PPDP 2006: 8th International ACM SIGPLAN Conference on Principles and Practice of Declarative Programming, pages 179-188, July 2006. [ bib | .ps | .pdf ]
[Mil06b] Dale Miller. Logic and logic programming: A personal account. ALP Newsletter, February 2006. Vol. 19, No. 1. [ bib | .pdf ]
[Mil06c] 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 ]
[Mil08a] Dale Miller. Formalizing operational semantic specifications in logic. Concurrency Column of the Bulletin of the EATCS, October 2008. [ bib | .pdf ]
[Mil08b] Dale Miller. A proof-theoretic approach to the static analysis of logic programs. In Festschrift for Peter Andrews, Studies in Logic. Elsevier, 2008. To appear. [ bib | .pdf ]
[MM97] Raymond McDowell and Dale Miller. A logic for reasoning with higher-order abstract syntax. In Glynn Winskel, editor, 12th Symp. on Logic in Computer Science, pages 434-445, Warsaw, Poland, July 1997. IEEE Computer Society Press. [ bib ]
[MM00] Raymond McDowell and Dale Miller. Cut-elimination for a logic with definitions and induction. Theoretical Computer Science, 232:91-119, 2000. [ bib ]
[MM02] 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 ]
[MMP96] Raymond McDowell, Dale Miller, and Catuscia Palamidessi. Encoding transition systems in sequent calculus: Preliminary report. Electronic Notes in Theoretical Computer Science, 3, 1996. [ bib ]
[MMP03] Raymond McDowell, Dale Miller, and Catuscia Palamidessi. Encoding transition systems in sequent calculus. Theoretical Computer Science, 294(3):411-437, 2003. [ bib | .dvi | .ps | .pdf ]
[MN85] Dale Miller and Gopalan Nadathur. A computational logic approach to syntax and semantics. Presented at the Tenth Symposium of the Mathematical Foundations of Computer Science, IBM Japan, May 1985. [ bib ]
[MN86a] Dale Miller and Gopalan Nadathur. Higher-order logic programming. In Ehud Shapiro, editor, Proceedings of the Third International Logic Programming Conference, pages 448-462, London, June 1986. [ bib ]
[MN86b] Dale Miller and Gopalan Nadathur. Some uses of higher-order logic in computational linguistics. In Proceedings of the 24th Annual Meeting of the Association for Computational Linguistics, pages 247-255. Association for Computational Linguistics, Morristown, New Jersey, 1986. [ bib ]
[MN87a] Dale Miller and Gopalan Nadathur. λProlog Version 2.6. Distribution in C-Prolog sources, August 1987. [ bib ]
[MN87b] Dale Miller and Gopalan Nadathur. A logic programming approach to manipulating formulas and programs. In Seif Haridi, editor, IEEE Symposium on Logic Programming, pages 379-388, San Francisco, September 1987. [ bib | .pdf ]
[MN88] Dale Miller and Gopalan Nadathur. λProlog Version 2.7. Distribution in C-Prolog and Quintus sources, July 1988. [ bib | http ]
[MN07] 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 ]
[MN08] Dale Miller and Vivek Nigam. Proofs with tables. Available via the authors web pages, 2008. [ bib ]
[MNPS91] Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Uniform proofs as a foundation for logic programming. Annals of Pure and Applied Logic, 51:125-157, 1991. [ bib ]
[MNS87] Dale Miller, Gopalan Nadathur, and Andre Scedrov. Hereditary Harrop formulas and uniform proof systems. In David Gries, editor, Symposium on Logic in Computer Science, pages 98-105, Ithaca, NY, June 1987. [ bib ]
[MP99] Dale Miller and Catuscia Palamidessi. Foundational aspects of syntax. ACM Computing Surveys, 31, September 1999. [ bib ]
[MP02] Dale Miller and Elaine Pimentel. Using linear logic to reason about sequent systems. In Uwe Egly and Christian G. Fermüller, editors, International Conference on Automated Reasoning with Analytic Tableaux and Related Methods, volume 2381 of LNCS, pages 2-23. Springer, 2002. [ bib | .dvi | .pdf ]
[MP04] Dale Miller and Elaine Pimentel. Linear logic as a framework for specifying sequent calculus. In Jan van Eijck, Vincent van Oostrom, and Albert Visser, editors, Logic Colloquium '99: Proceedings of the Annual European Summer Meeting of the Association for Symbolic Logic, Lecture Notes in Logic, pages 111-135. A K Peters Ltd, 2004. [ bib | .dvi | .ps | .pdf ]
[MS05] Dale Miller and Alexis Saurin. A game semantics for proof search: Preliminary results. In Dan Ghica and Guy McCusker, editors, GaLoP 2005: Games for Logic and Programming Languages, 2005. [ bib ]
[MS06] 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 Electr. Notes Theor. Comput. Sci, pages 543-563, 2006. [ bib | .pdf ]
[MS07] 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 ]
[MT02] Dale Miller and Alwen Tiu. Encoding generic judgments. In Proceedings of FSTTCS, number 2556 in LNCS, pages 18-32. Springer-Verlag, December 2002. [ bib | .dvi | .pdf ]
[MT03] Dale Miller and Alwen Tiu. A proof theory for generic judgments: An extended abstract. In Phokion Kolaitis, editor, 18th Symp. on Logic in Computer Science, pages 118-127. IEEE, June 2003. [ bib | .dvi | .ps | .pdf ]
[MT05] Dale Miller and Alwen Tiu. A proof theory for generic judgments. ACM Trans. on Computational Logic, 6(4):749-783, October 2005. [ bib | .pdf ]
[NM88] Gopalan Nadathur and Dale Miller. An Overview of λProlog. In Fifth International Logic Programming Conference, pages 810-827, Seattle, August 1988. MIT Press. [ bib | .pdf ]
[NM90] Gopalan Nadathur and Dale Miller. Higher-order Horn clauses. Journal of the ACM, 37(4):777-814, October 1990. [ bib ]
[NM98] Gopalan Nadathur and Dale Miller. Higher-order logic programming. In Dov M. Gabbay, C. J. Hogger, and J. A. Robinson, editors, Handbook of Logic in Artificial Intelligence and Logic Programming, volume 5, pages 499-590. Clarendon Press, Oxford, 1998. [ bib ]
[NM08a] Vivek Nigam and Dale Miller. Focusing in linear meta-logic. In Proceedings of IJCAR: International Joint Conference on Automated Reasoning, volume 5195 of LNAI, pages 507-522. Springer, 2008. [ bib | http ]
[NM08b] Vivek Nigam and Dale Miller. Focusing in linear meta-logic: Extended report. Available from http://hal.inria.fr/inria-00281631, 2008. [ bib ]
[PM90] Remo Pareschi and Dale Miller. Extending definite clause grammars with scoping constructs. In David H. D. Warren and Peter Szeredi, editors, 1990 International Conference in Logic Programming, pages 373-389. MIT Press, June 1990. [ bib ]
[PM05] 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 ]
[SBM07] Zach Snow, David Baelde, and Dale Miller. Taci: an interactive theorem proving framework. 2007. [ bib | http ]
[TM04] Alwen Tiu and Dale Miller. A proof search specification of the π-calculus. In 3rd Workshop on the Foundations of Global Ubiquitous Computing, volume 138 of ENTCS, pages 79-101, September 2004. [ bib | .pdf ]
[TM08] Alwen Tiu and Dale Miller. Proof search specifications of bisimulation and modal logic for the π-calculus. Submitted May 2008., 2008. [ bib ]
[TNM05] 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 ]
[ZMP05] Axelle Ziegler, Dale Miller, and Catuscia Palamidessi. A congruence format for name-passing calculi. In Structural Operational Semantics (SOS'05), Electronic Notes in Theoretical Computer Science, pages 169-189, Lisbon, Portugal, July 2005. Elsevier Science B.V. [ bib | .pdf ]

This file has been generated by bibtex2html 1.88.