Publications & Talks 
Lists of references of Dale Miller
via
DBLP,
Google
Scholar profile page, and MS Academic Search.
Complete list of BibTeX references sorted
by date and
by key.
 
Year  
Major venues 
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
 
Drafts 
Formalization of the BisimulationUpTo 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, 1926 July 2011.
Draft dated 23 July 2012: pdf.
A multifocused 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.


2013 
Extracting Proofs from Tabled Proof Search by Dale Miller and
Alwen Tiu.
CPP 2013:
Certified Proofs and Programs, LNCS 8307, pp. 194210.
(pdf,
HAL).
Foundational Proof Certificates: Making proof universal and permanent by Dale Miller.
An invited talk at LFMTP
2013: Logical Frameworks and MetaLanguages: Theory and
Practice, Boston, 23 September 2013:
abstract,
slides.
Checking foundational proof certificates for firstorder logic
(extended abstract) by Zakaria Chihani, Dale Miller, and Fabien
Renaud. Proceedings of PxTP
2014: Proof Exchange for Theorem Proving, 910 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 firstorder logic by
Zakaria Chihani, Dale Miller, and Fabien Renaud. Proceedings of
CADE 2013, LNAI
7898, pp. 162177 (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. 98116 (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", 2731 January 2013, Les
Diablerets, Switzerland.
Preserving differential privacy under finiteprecision semantics by Ivan
Gazeau, Dale Miller, and Catuscia
Palamidessi. Proceedings
of QAPL 2013.
Version dated 23 April 2013: pdf.
Version available
from HAL.


2012 
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 twolevel logic approach to reasoning about computations by
Andrew Gacek, Dale Miller, and Gopalan Nadathur.
Journal of Automated Reasoning, 49(2) (2012), pp. 241273
(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 183197 (LIPICS).
Draft dated 8 April 2012 (pdf).
Nonlocal 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
preproceedings of QFM 2012.
A full version is available: pdf.
A nonlocal method for robustness analysis of floating point
programs by Ivan Gazeau, Dale Miller, and Catuscia Palamidessi.
In the Proceedings
of QAPL
2012 (doi).


2011 
A proposal for broad spectrum proof certificates by Dale
Miller. CPP
2011: First International Conference on Certified
Proofs and Programs, 79 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 48, 2011.


2010 
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 twolevels 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. 3446 (pdf).
Slides pdf.
Fixed points and proof theory by Dale Miller.
FICS 2010: 7th
Workshop on Fixed Points in Computer Science, 2122 August
2010, Brno, Czech Republic. Slides: (pdf).
A framework for proof systems by Vivek Nigam and Dale Miller.
Journal of Automated Reasoning, 45(2), 157188.
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.
ACMBCS
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).


2009 
Focusing and Polarization in Linear, Intuitionistic, and Classical
Logic by Chuck
Liang and Dale Miller.
Theoretical Computer Science, 410(46), pp. 47474768 (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 ANRPrelude 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. 129140.
Also (pdf).


2008 
Relations: their uses in programming and computational
specifications by Dale Miller. Slides used during the Journees
du projet PEPSRelations 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 ProofTheoretic 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 MultiFocusing 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 383396. Boston: Springer, September
2008. (pdf).
Focusing in linear metalogic by Vivek Nigam and Dale Miller.
Proceedings of the International Joint Conference on Automated Reasoning,
(IJCAR 2008), LNCS 5195, pp. 507522. (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. 498508.
(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. 3344.
(pdf, arXiv)


2007 
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
451465.
SpringerVerlag
(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
466480.
SpringerVerlag.
(pdf).


2006 
Roadmap for enhanced languages and methods to aid verification,
Gary T. Leavens, JeanRaymond Abrial, Don Batory, Michael Butler, Alessandro
Coglio, Kathi Fisler, Eric Hehner, Cliff Jones, Dale Miller, Simon
PeytonJones, Murali Sitaraman, Douglas R. Smith, and Aaron Stump.
Technical Report TR #0621, 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 SpringerVerlag.
The slides from my talk.
Collection analysis for Horn clause programs: Extended
Abstract, by Dale Miller. Proceedings of PPDP'06 (Eighth
ACMSIGPLAN International Symposium on Principles and Practice of
Declarative Programming), 1012 July 2006, Venice, Italy. (pdf, ps)
© ACM, 2005.
HAL.
Logic and Logic Programming: a personal account, by Dale Miller.
Prepared for the Newsletter
of the Association
for Logic Programming, November 2005
(pdf,
ps,
html).
Published in the February 2006 issue
(Vol. 19 n. 1).


2005 
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 HigherOrder 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. 749783, 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. 15 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 namepassing 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 (1821 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.  
2004 
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 79101.
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).
Overview of linear logic programming,
by Dale Miller.
In
Linear Logic in Computer Science, edited by Thomas
Ehrhard, JeanYves Girard, Paul Ruet, and Phil Scott. Cambridge
University Press. London Mathematical Society Lecture Note, Volume 316.
(ps,
dvi,
pdf).


2003 
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. 118127.
(pdf, PS,
dvi).
Encryption as an abstract datatype: An extended abstract,
by Dale Miller.
FCS 2003: Foundations of
Computer Security. Edited by Iliano Cervesato, pp. 314, 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), 411437 (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).


2002 
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 SpringerVerlag.
Higherorder quantification and proof search by
Dale Miller. Proceedings of AMAST 2002, LNCS, edited by
Helene Kirchner (pdf).
© Copyright SpringerVerlag.
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 SpringerVerlag.
Slides used at talk.
Reasoning with HigherOrder Abstract Syntax in a Logical
Framework, by Raymond McDowell and Dale Miller. ACM
Transactions
on Computational Logic, 3(1) (January 2002), 80  136 (pdf).


2001 
Encoding Generic Judgments: Preliminary results, by Dale
Miller. Merlin 2001, a
workshop associated with IJCAR 2001, Siena, June 2001. (ps, pdf). Appears in ENTCS, Volume
58, Issue 1.


2000 
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 SpringerVerlag.
CutElimination 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.


1999 
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 MarchettiSpaccamela and Peter Wegner, Vol. 31,
September 1999.
(DVI,
PostScript,
pdf).


1998  
1997 
Review of Advances in Linear Logic, edited by JeanYves
Girard, Yves Lafont, Laurent Regnier.
J. of Symbolic Logic, 62 (2) 1997, pages 678680.
(pdf).
A Logic for Reasoning with HigherOrder Abstract Syntax, by
Raymond McDowell and Dale Miller. Proceedings of LICS'97, Warsaw, 434
 445.
(PostScript),
(pdf).
Sequent Calculus and the Specification of Computation,
School Marktoberdorf on Logic of Computation in 1997: An Advanced Study
Institute of the NATO Science Committee and the Technical University
of Munich, Germany.
(DVI,
pdf,
Postscript)


1996 
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 MultipleConclusion Specification Logic, by Dale Miller.
Theoretical Computer Science 165(1): 201232 (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


1995 
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).
Observations about using logic as a specification language,
by Dale Miller.
Invited paper to the GULPPRODE'95: Joint Conference on Declarative
Programming, Marina di Vietri (SalernoItaly), 1114 September 1995.
(HTML,
pdf,
PostScript,
Abstract).


1994 
Logic Programming in a Fragment of Intuitionistic Linear Logic
by Joshua S. Hodas and Dale Miller. Journal of Information and
Computation, 110(2):327365, 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 MultipleConclusion MetaLogic, by Dale Miller.
Proceedings of the 1994 Symposium on Logics in Computer Science,
edited by S. Abramsky, pp. 272281.
(DVI,
PostScript,
pdf,
Abstract).


1993 
A Proposal for Modules in λProlog, by Dale Miller.
Proceedings of the 1993 Workshop on Extensions to
Logic Programming, edited by Roy Dyckhoff, SpringerVerlag,
Lecture Notes in Computer Science, Vol. 798, 1994, pp. 206221.
(PostScript,
pdf,
Abstract).


1992 
Unification under a mixed prefix, by Dale Miller.
Journal of Symbolic Computation, Vol. 14 (1992), 321358.
(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. SpringerVerlag, LNCS
660, pp. 242265.
(DVI,
PostScript,
pdf,
Abstract).
Logic, Higherorder, 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, HigherOrders, and
Linear Logic. Given at the Fourth International School for
Computer Science Researchers, Acireale, Sicily, 29 June  3 July 1992
(86 pages). (pdf)


1991 
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. 3242.
(TR).
Selected in 2011 for
a TestofTime Award
(En
français).
Unification of Simply Typed LambdaTerms 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 LambdaAbstraction, 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, SpringerVerlag.
(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.


1990 
From Operational Semantics to Abstract Machines, John Hannan
and Dale Miller.
Journal of Mathematical Structures in Computer Science,
Vol. 2, No. 4 (1992), 415459. 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 MSCIS9059.
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. 373389, 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. 511526, 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)
Higherorder Horn Clauses, by Gopalan Nadathur and Dale Miller,
Journal of the ACM, Vol. 37, No. 4 (1990), 777814.
(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 DependentType λ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. 221235, LNAI 449, 1990.
(pdf)




1980's 
A Logic Programming Language with LambdaAbstraction, Function
Variables, and Simple Unification: Extended Abstract, by Dale Miller.
In the Proceedings of the 1989 Banff meeting on "HigherOrders",
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. 239255, 1989. UPenn CIS
technical report MSCIS8928
(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 810827,
Seattle, Washington, August 1988. MIT Press.
(DVI,
PostScript,
PDF)
Specifying theorem provers in a higherorder 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. 6180,
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, 98105.
A Compact Representation of Proofs, by Dale Miller.
Studia Logica, Volume 46, Number 4, pp. 347370, 1987.
(Postscript,
DVI,
pdf)
Proof Explanation and Revision, by Amy Felty and Dale Miller.
University of Pennsylvania, Technical Report MSCIS8817, 1987.
(Postscript)
Review of "The Art of Prolog" by Leon Sterling and Ehud Shapiro.
Computing Reviews, 349  350, July 1987.
Some uses of higherorder 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, 106114.
(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. 169192. Published by the American
Mathematical Society, 1984.
(pdf)
Proofs in HigherOrder Logic, by Dale Miller.
PhD Carnegie Mellon University, Department of Mathematics.
University of Pennsylvania technical report MSCIS8337.
(pdf)


1970's 
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.


Content 