List
of references at the
Bibliography Server on Database Systems & Logic Programming.
Complete list of BibTeX references sorted
by date and
by key.
A Focused Approach to Combining Logics by
Chuck Liang and Dale Miller.
Submitted 6 February 2010:
(pdf).
GIL: A Generalization of Intuitionistic Logic by
Chuck Liang and
Dale Miller. Submitted 15 January 2010:
(pdf).
A two-level logic approach to reasoning about computations by
Andrew Gacek, Dale Miller, and Gopalan Nadathur. Submitted 16
November 2009: (pdf).
Nominal abstraction by Andrew Gacek, Dale Miller, and
Gopalan Nadathur. Submitted 4 August 2009: (pdf, arXiv)
A framework for proof systems by Vivek Nigam and Dale Miller.
Accepted to the Journal of Automated Reasoning. Draft
dated 22 Dec 2009: (pdf)
Focused Inductive Theorem Proving by David Baelde, Dale Miller,
and Zachary Snow. IJCAR 2010, part of
FLoC 2010.
Draft dated 22 January 2010: (pdf).
Finding Unity in Computational Logic by Dale Miller.
ACM-BCS
Visions of Computer Science 2010
conference (pdf).
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,
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 and Dale Miller. ACM SIGPLAN Conference on Principles
and Practice of Declarative Programming (PPDP), pp. 129-140.
(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)
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).
Linear Logic by Roberto Di
Cosmo and Dale Miller. The Stanford
Encyclopedia of Philosophy (Fall
2006 Edition), Edward N. Zalta (ed.).
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.
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).
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).
Overview of linear logic programming,
by Dale Miller.
In
Linear Logic in Computer Science, edited by Thomas
Ehrhard, Jean-Yves Girard, Paul Ruet, and Phil Scott. Cambridge
University Press. London Mathematical Society Lecture Note, Volume 316.
(ps,
dvi,
pdf).
Proof Search Foundations for Logic Programming. Slides of invited
lectures at WOLLIC 2003.
(pdf)
Wollic 2003: 10th Workshop on Logic, Language, Information and
Computation, 29 July - 1 August 2003, Ouro Preto, Minas Gerais,
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.
Reasoning with Higher-Order Abstract Syntax in a Logical
Framework, by Raymond McDowell and Dale Miller. ACM
Transactions
on Computational Logic, 3(1) (January 2002), 80 - 136 (pdf).
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.
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).
A Logic for Reasoning with Higher-Order 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)
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).
Observations about using logic as a specification language,
by Dale Miller.
Invited paper to the GULP-PRODE'95: Joint Conference on Declarative
Programming, Marina di Vietri (Salerno-Italy), 11-14 September 1995.
(HTML,
pdf,
PostScript,
Abstract).
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 Multiple-Conclusion Meta-Logic, by Dale Miller.
Proceedings of the 1994 Symposium on Logics in Computer Science,
edited by S. Abramsky, pp. 272-281.
(DVI,
PostScript,
pdf,
Abstract).
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).
Proceedings of the 1993 International Logic Programming
Symposium, Vancouver, Canada, October 1993. Edited by Dale Miller.
Published by MIT Press.
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,
DVI,
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.
Proceedings of the Workshop on the λProlog Programming
Language, University of Pennsylvania, July 1992. Edited by Dale
Miller. Available as UPenn CIS technical report MS-CIS-92-86.
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)
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.
Meta-Programming in λProlog.
UKALP meeting, Edinburgh, 10 April 1991 (36 pages) (pdf).
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
appearred 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.
 |
Now for some of my earlier work. |
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)
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)
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
)
Proofs in Higher-Order Logic, by Dale Miller.
PhD Carnegie Mellon University, Department of Mathematics.
University of Pennsylvania technical report MS-CIS-83-37.
(pdf)
Observations in Pure Mathematics, by Dale Miller.
Paper for the 33rd Westinghouse Science Talent Search,
1974 (now called 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, and
this.
A computer generated proof of this identity is reported
here.