|Publications & Talks|
amast: 2002 | apal: 1991 2010 2011 2013 | cade: 1988 1990 2007 2013 | csl: 2004 2007a 2007b 2007c 2012 | ic: 2011 1994 | iclp: 1988 1989 1990a 1990b 1991 | ijcar: 2001 2006 2008 2010 2012 | jacm: 1990 | jar: 2009 2012 | jlc: 1991 | jlp: 1989 | jsc: 1992 | lics: 1987 1991 1994 1997 2003 2008a 2008b 2009 2013 | lpar: 2005 2007 | mfps: 2005 | mscs: 1992 | ppdp: 2006 2009 | slp: 1986 1987 | sos: 2005 2008 | studia: 1987 | tableaux: 2002 | tcs: 1995 2000 2003 2009 2013 | tocl: 2002 2005 2010
Formalization of the Bisimulation-Up-To Technique and its Meta Theory by Kaustuv Chaudhuri, Matteo Cimini, and Dale Miller. Draft dated 12 October 2013. Supporting material for his paper is available.
Extending Intuitionistic Logic for Sequential Control by Chuck Liang and Dale Miller. Draft dated 6 April 2012. Longer version of paper with proofs: pdf.
Communicating and trusting proofs: The case for foundational proof certificates by Dale Miller. To appear in the Proceedings of the 14th Congress of Logic, Methodology and Philosophy of Science in Nancy, France, 19-26 July 2011. Draft dated 23 July 2012: pdf.
A multi-focused proof system isomorphic to expansion proofs by Kaustuv Chaudhuri, Stefan Hetzl, and Dale Miller. Accepted to a special issue of the J. of Logic and Computation in honor of Roy Dyckhoff. Version dated 21 December 2012: pdf.
Extracting Proofs from Tabled Proof Search by Dale Miller and Alwen Tiu. CPP 2013: Certified Proofs and Programs, LNCS 8307, pp. 194-210. (pdf, HAL).
Foundational Proof Certificates: Making proof universal and permanent by Dale Miller. An invited talk at LFMTP 2013: Logical Frameworks and Meta-Languages: Theory and Practice, Boston, 23 September 2013: abstract, slides.
Checking foundational proof certificates for first-order logic (extended abstract) by Zakaria Chihani, Dale Miller, and Fabien Renaud. Proceedings of PxTP 2014: Proof Exchange for Theorem Proving, 9-10 June 2013, Lake Placid, USA. Version dated 22 April 2013: pdf.
Unifying Classical and Intuitionistic Logics for Computational Control by Chuck Liang and Dale Miller. Proceedings of LICS 2013. Version dated 25 May 2013: pdf.
Foundational proof certificates in first-order logic by Zakaria Chihani, Dale Miller, and Fabien Renaud. Proceedings of CADE 2013, LNAI 7898, pp. 162--177 (2013). Version dated 1 April 2013: pdf. The λProlog implementation of the proof checking framework reported in that paper is available.
A formal framework for specifying sequent calculus proof systems by Dale Miller and Elaine Pimentel. Theoretical Computer Science, Volume 474, February 2013, pp. 98-116 (doi). Draft dated 6 November 2012.
Talks on Foundational Proof Certificates: Slides used at the Freie Universität Berlin on 22 February 2013. Slides used during the CUSO Winter School on ``Proof and Computation", 27-31 January 2013, Les Diablerets, Switzerland.
Preserving differential privacy under finite-precision semantics by Ivan Gazeau, Dale Miller, and Catuscia Palamidessi. Proceedings of QAPL 2013. Version dated 23 April 2013: pdf. Version available from HAL.
Proceedings of the 8th Workshop on Fixed Points in Computer Science (FICS 2012) edited by Dale Miller and Zoltan Esik. Published as EPTCS 77, Feb 2012: pdf.
A two-level logic approach to reasoning about computations by Andrew Gacek, Dale Miller, and Gopalan Nadathur. Journal of Automated Reasoning, 49(2) (2012), pp. 241-273 (doi). Draft dated 30 August 2010: pdf, arXiv.
A Systematic Approach to Canonicity in the Classical Sequent Calculus by Kaustuv Chaudhuri, Stefan Hetzl, and Dale Miller. Proceedings of CSL 2012, pp 183-197 (LIPICS). Draft dated 8 April 2012 (pdf).
Non-local robustness analysis via rewriting techniques by Ivan Gazeau, Dale Miller, and Catuscia Palamidessi. A version of this paper (dated dated 1 August 2012) appeared in the pre-proceedings of QFM 2012. A full version is available: pdf.
A proposal for broad spectrum proof certificates by Dale Miller. CPP 2011: First International Conference on Certified Proofs and Programs, 7-9 December 2011, Taiwan. Draft dated 30 October 2011: (pdf). Slides: pdf. See also the description of the panel on Communicating and trusting proofs held during this meeting.
Towards a broad spectrum proof certificate by Dale Miller. Talk given at McGill and CMU in Oct 2010. (pdf).
Sequent Calculus: overview and recent developments by Dale Miller. Three hours of lectures during PLS8: 8th Panhellenic Logic Symposium, Ioannina, Greece, July 4-8, 2011.
A Focused Approach to Combining Logics by Chuck Liang and Dale Miller. Annals of Pure and Applied Logic 162(9): 679-697 (2011) (doi). Draft dated 13 Dec 2010: pdf.
Linear Logic by Roberto Di Cosmo and Dale Miller. The Stanford Encyclopedia of Philosophy, Edward N. Zalta (ed.). Current version. Fall 2006 Edition.
Reasoning about computations using two-levels of logic by Dale Miller. APLAS 2010: Eighth Asian Symposium on Programming Languages and Systems, Shanghai Jiao Tong University, China, 28 November - 1 December 2010. LNCS 6461, pp. 34-46 (pdf). Slides pdf.
Fixed points and proof theory by Dale Miller. FICS 2010: 7th Workshop on Fixed Points in Computer Science, 21-22 August 2010, Brno, Czech Republic. Slides: (pdf).
A framework for proof systems by Vivek Nigam and Dale Miller. Journal of Automated Reasoning, 45(2), 157-188. Draft dated 22 Dec 2009: (pdf)
Proof search when equality is a logical connective: Extended Abstract by Alexandre Viel and Dale Miller. PSTT 2010 workshop. Draft dated 22 April 2010: (pdf).
Focused Inductive Theorem Proving by David Baelde, Dale Miller, and Zachary Snow. IJCAR 2010, part of FLoC 2010 (pdf).
Towards a broad spectrum proof certificate by Dale Miller. MLPA 2010: 2nd Workshop on Module Systems and Libraries for Proof Assistants, part of FLoC 2010 (slides).
Finding Unity in Computational Logic by Dale Miller. ACM-BCS Visions of Computer Science 2010 conference (pdf). Slides
Proof search specifications of bisimulation and modal logics for the π-calculus by Alwen Tiu, Dale Miller. ACM Transactions on Computational Logic (TOCL), 11(2), 2010. Also (pdf, arXiv).
Focusing and Polarization in Linear, Intuitionistic, and Classical Logic by Chuck Liang and Dale Miller. Theoretical Computer Science, 410(46), pp. 4747-4768 (2009) (doi). Correction: Jean Pichon pointed out an error in Section 5 of this paper. The following version of the paper corrects that problem: (pdf). This paper is an extended version of a CSL07 paper.
Proof and refutation in MALL as a game, by Dale Miller. Slides used during the ANR-Prelude Workshop on Games, Dialogue, and Interaction at the University of Paris VIII, 29 September 2009.
Algorithmic specifications in linear logic with subexponentials by Vivek Nigam, Dale Miller. PPDP '09 Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming, 2009, pp. 129-140. Also (pdf).
Relations: their uses in programming and computational specifications by Dale Miller. Slides used during the Journees du projet PEPS-Relations 15 - 16 Dec 2008, Paris.
Formalizing operational semantic specifications in logic, by Dale Miller. Concurrency Column of the Bulletin of the EATCS, edited by Luca Aceto. October 2008. (pdf).
A Proof-Theoretic Approach to the Static Analysis of Logic Programs by Dale Miller. In Reasoning in Simple Type Theory: Festschrift in honour of Peter B. Andrews on his 70th birthday edited by Christoph Benzmueller, Chad E. Brown, Jörg Siekmann, and Richard Statman. Studies in Logic, Volume 17. Published by College Publications, December 2008. (pdf). A λProlog implementation of the static analysis checker described in this paper is available.
Canonical Sequent Proofs via Multi-Focusing by Kaustuv Chaudhuri, Dale Miller, and Alexis Saurin. Fifth IFIP International Conference on Theoretical Computer Science (TCS2008, Track B), volume 273 of IFIP International Federation for Information Processing, pages 383-396. Boston: Springer, September 2008. (pdf).
Focusing in linear meta-logic by Vivek Nigam and Dale Miller. Proceedings of the International Joint Conference on Automated Reasoning, (IJCAR 2008), LNCS 5195, pp. 507-522. (pdf). Extended version. Slides used at APS 2008 describing this paper.
Formalizing SOS specifications in logic by Dale Miller. Slides given during talk at SOS08, Reykjavik, Iceland, July 2008. (pdf)
A neutral approach to proof and refutation in MALL by Olivier Delande and Dale Miller. Proceedings of LICS 2008, edited by F. Pfenning, Pittsburgh, June 2008, pp. 498-508. (pdf).
Combining generic judgments with recursive definitions by Andrew Gacek, Dale Miller, and Gopalan Nadathur. Proceedings of LICS 2008, edited by F. Pfenning, Pittsburgh, June 2008, pp. 33-44. (pdf, arXiv)
An overview of a proof theoretical approach to reasoning about computation, by Dale Miller. A short annotated bibliography. Proceedings of LFMTP08, edited by A. Abel and C. Urban. (pdf, slides)
Least and greatest fixed points in linear logic by David Baelde and Dale Miller. LPAR 2007: Logic for Programming Artificial Intelligence and Reasoning (pdf). Extended version: pdf.
Focusing and Polarization in Intuitionistic Logic by Chuck Liang and Dale Miller. CSL'07: Computer Science Logic, J. Duparc and T. A. Henzinger, editors, LNCS 4646, pages 451-465. Springer-Verlag (pdf, slides). Extended versions of this paper: Dec 2006 and Sep 2007.
Incorporating tables into proofs by Dale Miller and Vivek Nigam. CSL'07: Computer Science Logic, J. Duparc and T. A. Henzinger, editors, LNCS 4646, pages 466-480. Springer-Verlag. (pdf).
From proofs to focused proofs: a modular proof of focalization in Linear Logic by Dale Miller and Alexis Saurin. CSL'07: Computer Science Logic, J. Duparc and T. A. Henzinger, editors, LNCS 4646, pages 405-419. Springer-Verlag. (pdf).
Roadmap for enhanced languages and methods to aid verification, 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. Technical Report TR #06-21, Department of Computer Science, Iowa State University, July 2006. (pdf)
Representing and reasoning with operational semantics, by Dale Miller. Invited paper to the Proceedings of IJCAR'06 (Third International Joint Conference on Automated Reasoning), 17 - 20 August 2006, Seattle. (pdf, dvi). © Copyright Springer-Verlag. The slides from my talk.
Collection analysis for Horn clause programs: Extended Abstract, by Dale Miller. Proceedings of PPDP'06 (Eighth ACM-SIGPLAN International Symposium on Principles and Practice of Declarative Programming), 10-12 July 2006, Venice, Italy. (pdf, ps) © ACM, 2005. HAL.
Mixing Finite Success and Finite Failure in an Automated Prover, by Alwen Tiu and Gopalan Nadathur and Dale Miller (pdf). Appears in ESHOL'05: Empirically Successful Automated Reasoning in Higher-Order Logics, 2 December (conference proceedings).
A Proof Theory for Generic Judgments, by Dale Miller and Alwen Tiu. ACM Transactions on Computational Logic, 6(4), pp. 749-783, October 2005. (dvi, ps, pdf).
On the specification of sequent systems, by Elaine Pimentel and Dale Miller. Proceedings of LPAR 2005: 12th International Conference on Logic for Programming, Artificial Intelligence and Reasoning. 2 - 6 December, Montego Bay, Jamaica. (pdf).
A Proof Theoretic Approach to Operational Semantics, by Dale Miller. The workshop proceedings of Algebraic Process Calculi: The First Twenty Five Years and Beyond. 1-5 August 2005, Bertinoro, Italy. Full proceedings of this meeting. Version of article in pdf to appear in ENTCS. Slides from talk.
A congruence format for name-passing calculi, by Axelle Ziegler, Dale Miller, and Catuscia Palamidessi. In the proceedings of SOS05: Structural Operational Semantics. Extended version with appendix: pdf. See also ENTCS Volume 156. HAL.
A game semantics for proof search: Preliminary results by Dale Miller and Alexis Saurin. Presented at MFPS 2005: Mathematical Foundations of Programming Semantics, Birmingham, UK (18-21 May) (pdf). See also ENTCS Volume 155. An earlier version was presented at GaLoP 2005: Games for Logic and Programming Languages. Here are slides for a talk I gave at Structure and Deduction on this same material.
A Proof Search Specification of the π-Calculus, by Alwen Tiu and Dale Miller. Proceedings of the Workshop on the Foundations of Global Ubiquitous Computing (FGUC 2004), Electronic Notes in Theoretical Computer Science Volume 138, Issue 1, 9 September 2004, pages 79-101. Conference paper and the extended version with proofs. See also the ENTCS page.
Linear logic as a framework for specifying sequent calculus, by Dale Miller and Elaine Pimentel. In the Logic Colloquium 1999. (ps, dvi, pdf).
Proof Search Foundations for Logic Programming. Slides of invited lectures at WOLLIC 2003. Wollic 2003: 10th Workshop on Logic, Language, Information and Computation, 29 July - 1 August 2003, Ouro Preto, Minas Gerais, (pdf)
A Proof Theory for Generic Judgments: An extended abstract, by Dale Miller and Alwen Tiu. Proceedings of LICS 2003, edited by P. Kolaitis. Ottawa, July 2003, pp. 118-127. (pdf, PS, dvi).
Encryption as an abstract data-type: An extended abstract, by Dale Miller. FCS 2003: Foundations of Computer Security. Edited by Iliano Cervesato, pp. 3-14, June 2003. (dvi, pdf,PS). Slides used for talk: pdf. Appears in ENTCS, Volume 84.
Encoding Transition Systems in Sequent Calculus, by Raymond McDowell, Dale Miller, and Catuscia Palamidessi. Theoretical Computer Science, 294(3), 411-437 (2003). (dvi, ps, pdf). A preliminary report appears in the Proceedings of the 1996 Workshop on Linear Logic and is available in Volume 3 of ENTCS (dvi, ps, pdf, Abstract).
Encoding Generic Judgments by Dale Miller and Alwen Tiu. Proceedings of FSTTCS 2002 (22nd Foundations of Software Technology and Theoretical Computer Science), edited by M. Agrawal and A. Seth (pdf, dvi). © Copyright Springer-Verlag.
Higher-order quantification and proof search by Dale Miller. Proceedings of AMAST 2002, LNCS, edited by Helene Kirchner (pdf). © Copyright Springer-Verlag. A subset of this talk was presented at the Linear Logic workshop, FLoC 2002 (see these slides for that presentation).
Using linear logic to reason about sequent systems by Dale Miller and Elaine Pimentel. Proceedings of Tableaux 2002, LNCS 2381, edited by Uwe Egly, Christian G. Fermller (dvi, pdf). © Copyright Springer-Verlag. Slides used at talk.
Abstract syntax for variable binders: An overview, by Dale Miller. Proceedings of Computation Logic 2000, LNAI 1861, edited by John Lloyd, et. al. (dvi, ps, pdf). © Copyright Springer-Verlag.
Cut-Elimination for a Logic with Definitions and Induction, by Raymond McDowell and Dale Miller. Theoretical Computer Science, volume 232, pages 91 - 119 (2000). (dvi, ps, pdf). Some comments and errata.
Foundational Aspects of Syntax, by Dale Miller and Catuscia Palamidessi. ACM Computing Surveys Symposium on Theoretical Computer Science: A Perspective, edited by Pierpaolo Degano and Roberto Gorrieri and Alberto Marchetti-Spaccamela and Peter Wegner, Vol. 31, September 1999. (DVI, PostScript, pdf).
Review of Advances in Linear Logic, edited by Jean-Yves Girard, Yves Lafont, Laurent Regnier. J. of Symbolic Logic, 62 (2) 1997, pages 678-680. (pdf).
A Logic for Reasoning with Higher-Order Abstract Syntax, by Raymond McDowell and Dale Miller. Proceedings of LICS'97, Warsaw, 434 - 445. (PostScript), (pdf).
Linear Logic as Logic Programming: An Abstract by Dale Miller. In Christian Retore (Ed.), Logical Aspects of Computational Linguistics, First International Conference, LACL'96. Nancy, France, September 1996 (pdf).
Forum: A Multiple-Conclusion Specification Logic, by Dale Miller. Theoretical Computer Science 165(1): 201-232 (1996). (DVI, pdf, PostScript, Abstract).
Logical Foundations for Open System Design: A position paper, by Dale Miller. ACM Computing Surveys 28(4es), December 1996, This article derives from a position statement prepared for the Workshop on Strategic Directions in Computing Research. HTML
A Survey of Linear Logic Programming, by Dale Miller. Computational Logic: The Newsletter of the European Network in Computational Logic, Volume 2, No. 2, December 1995, pp. 63 - 67. (HTML, PostScript, pdf, DVI).
Logic Programming in a Fragment of Intuitionistic Linear Logic by Joshua S. Hodas and Dale Miller. Journal of Information and Computation, 110(2):327-365, 1 May 1994. (DVI, PostScript, pdf, MathReview). Prolog code from this paper is available. An earlier version of this paper appeared in LICS'91.
A Proposal for Modules in λProlog, by Dale Miller. Proceedings of the 1993 Workshop on Extensions to Logic Programming, edited by Roy Dyckhoff, Springer-Verlag, Lecture Notes in Computer Science, Vol. 798, 1994, pp. 206-221. (PostScript, pdf, Abstract).
Unification under a mixed prefix, by Dale Miller. Journal of Symbolic Computation, Vol. 14 (1992), 321-358. (DVI, pdf, Abstract).
The π-calculus as a theory in linear logic: Preliminary results, by Dale Miller. Proceedings of the 1992 Workshop on Extensions to Logic Programming, edited by E. Lamma and P. Mello. Springer-Verlag, LNCS 660, pp. 242-265. (DVI, PostScript, pdf, Abstract).
Logic, Higher-order, by Dale Miller. A short article for the Encyclopedia of Artificial Intelligence: Second Edition, edited by S. Shapiro, 1992. (HTML, pdf).
Logic in Logic Programming: Sequent Calculus, Higher-Orders, and Linear Logic. Given at the Fourth International School for Computer Science Researchers, Acireale, Sicily, 29 June - 3 July 1992 (86 pages). (pdf)
Proceedings of the Workshop on Linear Logic and Logic Programming, Washington, DC, November 1992. Edited by Dale Miller. Available as UPenn CIS technical report MS-CIS-92-80.
Logic Programming in a Fragment of Intuitionistic Linear Logic: Extended Abstract, by Joshua Hodas and Dale Miller. LICS91: Sixth Annual Symposium on Logic in Computer Science, ed. G. Kahn, pp. 32-42. (TR). Selected in 2011 for a Test-of-Time Award (En français).
Unification of Simply Typed Lambda-Terms as Logic Programming, by Dale Miller. Eighth International Conference on Logic Programming, edited by Koichi Furukawa, Paris, France. MIT Press, June 1991, pp. 255 - 269. (DVI, pdf Abstract).
A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification, by Dale Miller. Journal of Logic and Computation, Vol. 1, No. 4 (1991), 497 - 536. (DVI, PostScript, pdf, Abstract).
Abstract Syntax and Logic Programming, by Dale Miller. Proceedings of the First and Second Russian Conferences on Logic Programming, September 1991, St. Petersburg, LNAI Series, Springer-Verlag. (DVI, pdf).
Uniform proofs as a foundation for logic programming, by Dale Miller, Gopalan Nadathur, Frank Pfenning, and Andre Scedrov. Annals of Pure and Applied Logic, Vol. 51 (1991), 125 - 157. (DVI, pdf, MathReview). Errata in DVI and pdf formats.
Proof Theory as an Alternative to Model Theory, by Dale Miller. A short article for the Newsletter of the ALP (Association for Logic Programming), August 1991. Also available here.
From Operational Semantics to Abstract Machines, John Hannan and Dale Miller. Journal of Mathematical Structures in Computer Science, Vol. 2, No. 4 (1992), 415-459. Earlier version of this paper appeared in Lisp and Functional Programming, 1990. (DVI, pdf, Abstract).
An Extension to ML to Handle Bound Variables in Data Structures, in the Proceedings of the Logical Frameworks BRA Workshop, May 1990. (DVI, Postscript, pdf, Abstract). University of Pennsylvania technical report MS-CIS-90-59.
Extending Definite Clause Grammars with Scoping Constructs, by Remo Pareschi and Dale Miller. In the Proceedings of the 1990 International Conference in Logic Programming, edited by David H. D. Warren and Peter Szeredi, pp. 373-389, MIT Press, June 1990. (DVI, pdf).
Representing Objects in a Logic Programming Language with Scoping Constructs, by Joshua Hodas and Dale Miller. In the Proceedings of the 1990 International Conference in Logic Programming, edited by David H. D. Warren and Peter Szeredi, pp. 511-526, MIT Press, June 1990. (DVI, PS).
Abstractions in logic programming, by Dale Miller. Logic and Computer Science, edited by Peirgiorgio Odifreddi, Academic Press, pp. 329 - 359, 1990. (DVI, pdf)
Higher-order Horn Clauses, by Gopalan Nadathur and Dale Miller, Journal of the ACM, Vol. 37, No. 4 (1990), 777-814. (DVI, pdf, MathReview).
Review of "A computational logic" and "A computational logic handbook" by Robert Boyer and J. Strother Moore. Journal of Symbolic Logic, September 1990, 1302 - 1304.
Encoding a Dependent-Type λ-Calculus in a Logic Programming Language, by Amy Felty and Dale Miller. In the Proceedings of the 1990 Conference on Automated Deduction, edited by Mark Stickel, pp. 221-235, LNAI 449, 1990. (pdf)
A Logic Programming Language with Lambda-Abstraction, Function Variables, and Simple Unification: Extended Abstract, by Dale Miller. In the Proceedings of the 1989 Banff meeting on "Higher-Orders", edited by Graham M. Birtwistle, Banff, Canada, 23 - 28 September 1989. (pdf).
Lexical Scoping as Universal Quantification, by Dale Miller. In the Proceedings of the 1989 International Conference in Logic Programming, edited by G. Levi and M. Martelli, pp. 268 - 283, MIT Press, June 1989. (DVI,Postscript, pdf).
Deriving Mixed Evaluation from Standard Evaluation for a Simple Functional Language, by John Hannan and Dale Miller. In the Proceedings of the Mathematics of Program Construction, edited by Jan L. A. van de Snepscheut, pp. 239-255, 1989. UPenn CIS technical report MS-CIS-89-28 (pdf).
A logical analysis of modules in logic programming, by Dale Miller. Journal of Logic Programming, 6 (1989), 79 - 108. Translated to Russian and reprinted in Mathematical Logic in Programming, edited by Y. I. Janov, M. V. Zakhar'yashchev, and A. Voronkov, Mir Publishers, USSR, 1991, pp. 233 - 273). (DVI, pdf)
A Meta Language for Type Checking and Inference: An Extended Abstract by Amy Felty and Dale Miller. Proc. of the 1989 Workshop on Programming Logic, 1989, Båstad, Sweden. (pdf)
An overview of λProlog. by Gopalan Nadathur and Dale Miller. Fifth International Logic Programming Conference, In Kenneth A. Bowen and Robert A. Kowalski, editors, pages 810-827, Seattle, Washington, August 1988. MIT Press. (DVI, PostScript, PDF)
Specifying theorem provers in a higher-order logic programming language, by Amy Felty and Dale Miller. In the Proceedings of the 1988 Conference on Automated Deduction, edited by Ewing Lusk and Ross Overbeck, pp. 61-80, LNCS 310, May 1988. (pdf)
A logic programming approach to manipulating formulas and programs, by Dale Miller and Gopalan Nadathur. IEEE Symposium on Logic Programming, San Francisco, September 1987, 379 - 388. (Abstract, PostScript, pdf)
Hereditary Harrop formulas and uniform proofs systems, by Dale Miller, Gopalan Nadathur, Andre Scedrov. Second Annual Symposium on Logic in Computer Science, Program Chair David Gries, Cornell University, June 1987, 98-105.
A Compact Representation of Proofs, by Dale Miller. Studia Logica, Volume 46, Number 4, pp. 347-370, 1987. (Postscript, DVI, pdf)
Proof Explanation and Revision, by Amy Felty and Dale Miller. University of Pennsylvania, Technical Report MS-CIS-88-17, 1987. (Postscript)
Review of "The Art of Prolog" by Leon Sterling and Ehud Shapiro. Computing Reviews, 349 - 350, July 1987.
Some uses of higher-order logic in computational linguistics, by Dale Miller and Gopalan Nadathur. 24th Annual Meeting of the Association for Computational Linguistics, New York, June 1986, 247 - 255. (DVI, PostScript, PDF)
A Theory of Modules for Logic Programming, by Dale Miller. Third Annual IEEE Symposium on Logic Programming, Salt Lake City, September 1986, 106-114. (PDF)
An Integration of Resolution and Natural Deduction Theorem Proving, by Amy Felty and Dale Miller. 1986 National Conference on Artificial Intelligence ( pdf )
Automating higher order logic, by Peter Andrews, Eve Longini Cohen, Dale Miller, and Frank Pfenning. In Automated Theorem Proving: After 25 Years, edited by W. W. Bledsoe and D. W. Loveland, pp. 169--192. Published by the American Mathematical Society, 1984. (pdf)
Observations in Pure Mathematics, by Dale Miller. Paper for the 33rd Westinghouse Science Talent Search, 1974 (now the Intel Science Talent Search): (dvi, pdf). When I published my first mathematical result as an Advanced Problem in the Fibonacci Quarterly, my name was misread as D. A. Millin. The name was corrected when a solution was printed but it seems the misread name persists. To read about the Millin series, see this, this, this, this, and this. A computer generated proof of this identity is reported here.