Publications
Most journal, conference, and workshop publications by
Dale Miller
are available below. Publications as
books & proceedings and
technical reports &
short articles are also available.
For other lists of references, see
dblp,
hal,
Google Scholar,
Orcid,
ACM DL,
Semantic Scholar,
csauthors,
zbMATH,
YouTube,
Amazon, and
WoS.
(This list may soon surpass my publication list in length.)
A complete list of BibTeX references to my publications is also
available.
I maintain a Bibtex file that I use
in my writing projects.
Work in progress

PropertyBased Testing by Elaborating Proof Outlines by Dale
Miller and Alberto Momigliano. Submitted.
Draft dated 23 July 2023.

Proof theory, proof search, and logic programming by Dale
Miller. A monograph used in my graduate course lectures on proof
theory and linear logic. The
current draft is dated 25
August 2023 and is 262 pages long. Comments on this draft are
welcome.
To appear

Focusing Gentzen's LK proof system by Chuck Liang and Dale
Miller. To appear in Peter SchroederHeister on ProofTheoretic
Semantics in the Springer series Outstanding Contributions
to Logic, edited by Thomas Piecha and Kai Wehmeier.
(HAL).
Draft dated 28 March 2023
(first submitted April 2020).
This paper proves the main metatheory results for the LKFproof
system. A recorded lecture on this paper is
online.
Guillaume MunchMaccagnoni has offered some commentary on this paper
in the comment section
of this
blog post.
2023

Formal Reasoning using Distributed Assertions by Farah Al
Wardani, Kaustuv Chaudhuri, and Dale Miller. To appear in the
proceedings of FroCos
2023
(doi,
HAL).
Draft dated 21 July 2023.
An earlier version of this paper is available as a technical report on
HAL.

A system of inference based on proof search: an extended
abstract by Dale Miller. In the proceedings of LICS 2023.
Draft dated 5 May 2023
(doi,
hal).
My presentation used these slides.

A positive perspective on term representation by Dale Miller
and JuiHsuan Wu.
CSL 2023, pp. 3:13:21.
Draft dated
10 November 2022.
(doi,
hal).
Slides.

Peano Arithmetic and μMALL: An extended abstract
by Matteo Manighetti and Dale Miller.
Draft dated 2 August
2023. This paper was presented
at FICS
2023 using these slides and
at TLLALinearity
2022 using these slides.
Eariler drafts of this work appear as
this draft (dated 4 July
2022) and in the technical report Computational logic based on
linear logic and fixed points
(HAL, dated 18 Feb
2022).
2022

A Survey of the ProofTheoretic Foundations of Logic
Programming by Dale Miller. Invited submission to the
20th
Anniversary Issue of the
Theory
and Practice of Logic Programming (TPLP), 22(6), 859904. Published online November 2021.
(doi,
arXiv,
HAL).
Draft dated 29 October 2021.

A positive perspective on term representation: work in progress by Dale Miller
and JuiHsuan Wu.
Draft dated
2 September 2022.
Presented at LFMTP
2022 (slides).

Functionsasconstructors Higherorder Unification: Extended
Pattern Unification by Tomer Libal and Dale Miller.
Special Issue on Theoretical and Practical
Aspects of Unification in
the Annals
of Mathematics and Artificial Intelligence, 90(5), 455479
(doi,
HAL).
Draft dated 9 September 2021.

The undecidability of proof search when equality is a logical
connective by Dale Miller and Alexandre Viel.
Special Issue on Theoretical and Practical Aspects of
Unification in
the Annals
of Mathematics and Artificial Intelligence, 90(5), 523535
(doi,
HAL).
Also available online from the publisher.
Draft dated 18 June 2021.

From axioms to synthetic inference rules via focusing by Sonia
Marin, Dale Miller, Elaine Pimentel, and Marco Volpe.
Annals of Pure and Applied Logic 173(5), 21 January 2022
(doi,
HAL).
Draft dated 15 January
2022. Video
presentation by Sonia.
2021
2020

Extrinsically Typed Operational Semantics for Functional
Languages by Matteo Cimini, Dale Miller, and Jeremy Siek.
SLE 2020: ACM SIGPLAN
International Conference on Software Language Engineering.
Draft dated 12 November 2020.
(doi).
Video
presentation by Matteo.

Andre and the early days of Penn's Logic and Computation Group
by Dale Miller. Appears in Logic, Language, and Security:
ScedrovFest65, LNCS 12300
(doi).
Draft dated 20 May 2020.

Structural Proof Theory and Logic Programming: An extended
abstract by Dale Miller. Presented at
TeaseLP Workshop 2020.
Draft of abstract dated 15 May 2020.
Slides and
video
are available.

Focusing, axioms and synthetic inference rules (extended
abstract) by Elaine Pimentel, Sonia Marin, Dale Miller, and
Marco Volpe. Elaine gave an invited talk on this abstract
at IJCAR 2020.
She shared this talk with Sonia: see
their video.
Draft dated 19 April 2020.

FPCCoq: Using ELPI to elaborate external proof evidence into Coq
proofs by Roberto Blanco, Matteo Manighetti, and Dale Miller.
Accepted for
the Coq Workshop
2020.
A twopage abstract dated 27 April 2020.
A ``workinprogress'' abstract on this topic titled
Linking a λProlog proof checker to the Coq kernel: An
extended abstract was also accepted to
LFMTP 2020
(see the twopage abstract dated 7 June
2020).

On the Proof Theory of PropertyBased Testing of Coinductive
Specifications, or: PBT to Infinity and beyond by Roberto Blanco,
Dale Miller, and Alberto
Momigliano. A twopage abstract
(dated 5 Feb 2020) accepted for
TYPES 2020.
A ``workinprogress'' abstract on this topic was also accepted to
LFMTP 2020.

A distributed and trusted web of formal proofs by Dale Miller.
Draft dated 14 October 2019.
In the Proceedings
of 16th ICDCIT 2020:
International Conference on Distributed Computing and Internet
Technology, 912 January 2020, Kalinga Institute of Industrial
Technology, Bhubaneswar, Odisha, India. Springer LNCS 11969
(doi).
2019

My colleague, wife, and friend by Dale Miller.
In The Art of
Modelling Computational Systems: A Journey from Logic and Concurrency
to Security and Privacy. Essays Dedicated to Catuscia Palamidessi on
the Occasion of Her 60th Birthday. LNCS 11769. The cover art
for this volume was made
by our daughter Nadia
Miller. This volume was presented at a meeting held on the
campus of Ecole Polytechnique, 4 November 2019.
Draft dated 12 July 2019.

A proof theory for model checking by Quentin Heath and Dale Miller.
Draft dated 6 June 2018.
Journal of Automated Deduction, 64(4), 857885
(doi,
HAL).
A video based on this paper appears
online.

Mechanized metatheory revisited by Dale Miller.
Draft dated 30 September 2018.
Journal of Automated Reasoning, 63(3), pp. 625665 (October 2019).
(doi,
HAL).

Functional programming with λtree syntax by
Ulysse Gérard, Dale Miller, and Gabriel Scherer.
In PPDP 2019.
Draft dated 26 July 2019.
(HAL,
arXiv,
doi).
This
paper describes MLTS, an extension to (core) OCaml with features
for treating bound variables in syntactic expressions. You can try
writing and executing small MLTS programs in your web browser by
visiting
TryMLTS. Source files are
also available there.

PropertyBased Testing via Proof Reconstruction by Roberto
Blanco, Dale Miller, and Alberto Momigliano.
In PPDP 2019.
Draft dated 16 July 2019.
(HAL,
doi).

A prooftheoretic approach to certifying skolemization
by Kaustuv Chaudhuri, Matteo Manighetti, and Dale Miller.
In the proceedings
of CPP
2019. Draft dated 16 December 2018.
(doi,
HAL).
Supporting λProlog code can be found
on GitHub.
2018

Mechanized Metatheory Revisited: An Extended Abstract by Dale Miller.
Available from
the TYPES
2016 postproceedings.
Draft dated 6 July 2018.
(doi,
HAL).

Computationasdeduction in Abella: work in progress
by Kaustuv Chaudhuri, Ulysse Gérard, and Dale Miller.
Draft dated 26 May 2018.
LFMTP 2018:
Logical Frameworks and MetaLanguages: Theory and Practice, Oxford,
7 July 2018.
Slides.
Version on HAL.

Functional programming with λtree syntax: a progress report
by Ulysse Gérard and Dale Miller.
Draft dated 26 May 2018.
LFMTP 2018:
Logical Frameworks and MetaLanguages: Theory and Practice, Oxford,
7 July 2018.
Slides.
Version on HAL.

Influences between logic programming and proof theory by Dale Miller.
Draft of an extended
abstract dated 1 January 2018
(HAL). Presented
at HaPoP 2018:
Fourth Symposium on the History and
Philosophy of Programming, Oxford, 22 March 2018.
Slides.
2017

PropertyBased Testing via Proof Reconstruction: Workinprogress by Roberto
Blanco, Dale Miller, and Alberto Momigliano.
LFMTP 17:
Logical Frameworks and MetaLanguages: Theory and Practice 2017.
Draft dated 30 August 2017.
(HAL).

Linear logic as a logical framework by Dale Miller. An
abstract accepted for
SD 17: Structures and Deduction 2017.
Draft dated 26 July 2017.
(HAL).

Using linear logic and proof theory to unify computational
logic by Dale Miller. An abstract presented at
TLLA 17: Trends in
Linear Logic and Applications.
Draft dated 21 July 2017.
Slides.

Separating Functional Computation from Relations by
Ulysse Gérard and Dale Miller.
CSL
2017, page 23:123:17.
Draft dated 20 June 2017.
Slides based on this paper used in October 2018.
(doi,
HAL).

Translating between implicit and explicit versions of proof by
Roberto Blanco, Zak Chihani, and Dale
Miller. CADE26. pages 255273.
Draft dated 26 May 2017.
(doi,
HAL).

Proof checking and logic programming by Dale Miller.
Formal Aspects of Computing, May 2017, Volume 29, Issue 3,
pp 383399. (doi,
HAL).

A semantic framework for proof evidence by Zakaria Chihani,
Dale Miller, and Fabien Renaud. Journal of Automated
Reasoning, Volume 59, Issue 3, pp. 287330
Draft dated 21 June 2016.
Supporting λProlog code dated 2 May 2016.
(doi,
HAL)
2016

Classical polarizations yield double negation translations by
Zakaria Chihani, Danko Ilik, and Dale Miller.
Draft dated 5 January 2019.
Version on HAL dated
28 August 2016.

A Proof Theory for Model Checking: An Extended Abstract by Quentin Heath and Dale Miller.
Draft dated 31 October 2016.
A talk on the contents of this paper was given at
Linearity 2016
and at
LL2016 (Linear Logic:
interaction, proofs and computation, 710 November 2016, Lyon).
Slides. This paper also appears in
proceedings of this meeting:
see EPTCS
238.

A focused framework for emulating modal proof systems by
Sonia Marin, Dale Miller, and Marco Volpe. Proceedings of
AiML 2016.
Draft dated 12 June 2016.

Preserving differential privacy under finiteprecision semantics by
Ivan Gazeau, Dale Miller, and Catuscia
Palamidessi. TCS 655: 92108 (2016).
doi.
Draft dated 1 September 2014.
Version on HAL.

Proof Certificates for Equality Reasoning by
Zakaria Chihani and Dale Miller. Postproceedings
of LSFA
2015: 10th Workshop on Logical and Semantic Frameworks, with
Applications. Natal, Brazil.
(doi)
Draft dated 25 January 2016.
Version on HAL.

A multifocused proof system isomorphic to expansion proofs by
Kaustuv Chaudhuri, Stefan Hetzl, and Dale Miller.
A special issue of the J. of Logic and
Computation in honor of Roy Dyckhoff (26(2): 577603).
(doi).
Version dated 1 December 2013: pdf.

Functionsasconstructors Higherorder Unification by Tomer
Libal and Dale Miller. Proceedings of
to FSCD 2016.
Draft dated 15 April 2016.

WellTyped Languages are Sound
by Matteo Cimini, Dale Miller, and Jeremy G. Siek.
Draft dated 22 October 2016.
Also on arXiv.
2015

Proof Checking and Logic Programming by Dale Miller.
Postproceedings
of LOPSTR 2015, edited by Moreno Falaschi.
LNCS 9527, pp. 317 (doi).
An abstract appeared in the proceedings
of PPDP
2015, edited by Elvira Albert, p. 18
(doi).
Draft dated 16 October 2015: pdf.

Defining the meaning of TPTP formatted proofs by
Roberto Blanco, Tomer Libal, and Dale Miller. The Proceedings
of IWIL2015:
11th International Workshop on the Implementation of Logics, Fiji,
23 November 2015.
Draft dated 9 November 2015.

On Subexponentials, Synthetic Connectives, and MultiLevel
Delimited Control by Chuck Liang and Dale Miller.
The Proceedings of LPAR20.
November 2015. Springer LNCS 9450.
Draft dated 8 September 2015.
Version with appendices dated 8 September 2015.

Focused labeled proof systems for modal logic by Dale Miller
and Marco Volpe.
The Proceedings of LPAR20.
November 2015. Springer LNCS 9450.
The conference version and
an extended version (with
appendices) are available.
Version on HAL.

Proof Outlines as Proof Certificates: a system description by
Roberto Blanco and Dale Miller. In the Proceedings of the First
International Workshop on Focusing
(WoF
2015). EPTCS
volume 197. A draft dated Draft dated 1
November 2015.

A framework for proof certificates in finite state exploration by
Quentin Heath and Dale Miller. In the proceedings of
PxTP 2015
(doi).
Draft dated 25 June 2015.

Foundational Proof Certificates by Dale Miller.
In the proceedings
of All
about Proofs, Proofs for All (APPA), edited by D. Delahaye
and B. Woltzenlogel Paleo, pp. 150163.
Version dated 1 December 2014: pdf.

A lightweight formalization of the metatheory of bisimulationupto by
Kaustuv Chaudhuri, Matteo Cimini, and Dale Miller.
CPP 2015: Proceedings of the
2015 Conference on Certified Programs and Proofs, pp. 157166.
(doi).
Draft dated 10 December 2014.
Supporting
material: definitions, theorems, and proofs described in the
paper are formalized in Abella.

A proposal for multifocused LJF by Dale Miller.
Draft dated 26 April 2015.
2014

Communicating and trusting proofs:
The case for foundational proof certificates
by Dale Miller.
Proceedings
of the 14th Congress of Logic,
Methodology and Philosophy of Science in Nancy, France, 1926
July 2011. Edited by P. SchroederHeister, W. Hodges,
G. Heinzmann, and P. E. Bour, pp. 323342. Published by College
Publications, 2014.
Draft dated 13 March 2014: pdf.

Abella: A System for Reasoning about Relational Specifications by
David Baelde, Kaustuv Chaudhuri, Andrew Gacek, Dale Miller, Gopalan
Nadathur, Alwen Tiu, and Yuting Wang.
Journal of Formalized
Reasoning, Volume
7, Number 2 (2014). Draft dated 30 Dec 2014.

Automation of HigherOrder Logic by Christoph Benzmüller and Dale Miller.
Draft dated 16 March 2014.
Handbook of the History of Logic, Volume
9: Logic and Computation, edited by D. Gabbay, J. Siekmann,
and J. Woods (NorthHolland), pp. 215254.
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).

Checking foundational proof certificates for firstorder logic
(extended abstract) by Zakaria Chihani, Dale Miller, and Fabien
Renaud. Proceedings of PxTP
2013: Proof Exchange for Theorem Proving, 910 June 2013, Lake Placid, USA.
Version dated 22 April 2013: pdf.
Version on HAL.

Unifying Classical and Intuitionistic Logics for Computational Control by
Chuck Liang and Dale Miller. Proceedings
of LICS 2013.
Version dated 25 May 2013: pdf.
(HAL,
doi).

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.

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.
Version on HAL.

Preserving differential privacy under finiteprecision semantics by Ivan
Gazeau, Dale Miller, and Catuscia
Palamidessi.
Proceedings
of QAPL 2013.
Version dated 23 April 2013: pdf.
(HAL).

Kripke Semantics and Proof Systems for Combining Intuitionistic
Logic and Classical Logic by Chuck Liang and Dale Miller.
Annals of Pure and Applied Logic, 164(2):86111, February
2013 (doi).
Draft dated 7 October 2012: pdf.
Version on HAL.
2012

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.

A Focused Approach to Combining Logics by
Chuck Liang and Dale Miller.
Annals of Pure and Applied Logic 162(9): 679697 (2011)
(doi).
Draft dated 13 Dec 2010: pdf.

Nominal abstraction by Andrew Gacek, Dale Miller, and
Gopalan Nadathur. Information &
Computation, 209 (2011), pp. 4873.
Draft dated 22 September 2010:
(pdf,
arXiv).
2010

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.

A framework for proof systems by Vivek Nigam and Dale Miller.
Journal of Automated Reasoning, 45(2), 157188
(doi).
Draft dated 22 Dec 2009.

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 and
Dale Miller.
ACM Transactions on Computational Logic (TOCL), 11(2), 2010.
(pdf,
arXiv,
doi).

Proof and refutation in MALL as a game by Olivier Delande, Dale
Miller, and Alexis Saurin. Annals of Pure and Applied Logic,
161(5), February 2010, pp. 654672
(doi,
pdf).
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.

Algorithmic specifications in linear logic with subexponentials by
Vivek
Nigam and
Dale Miller.
PPDP '09 Proceedings of the 11th ACM SIGPLAN conference on Principles and practice of declarative programming, 2009, pp. 129140.
Also (pdf).

A Unified Sequent Calculus for Focused Proofs by Chuck Liang and
Dale Miller. Proceeding of LICS 09,
pp. 355364. (pdf)
2008

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.

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)

Reasoning in Abella about Structural Operational Semantics Specifications
by Andrew Gacek, Dale Miller, and Gopalan Nadathur.
Proceedings of LFMTP08,
edited by A. Abel and C. Urban.
(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.
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).

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 405419. SpringerVerlag. (pdf).

The Bedwyr system for model checking over syntactic expressions
by David Baelde, Andrew Gacek, Dale Miller, Gopalan Nadathur, and
Alwen Tiu. CADE 2007:
21th Conference on Automated Deduction, Frank Pfenning, editor,
LNAI 4603, pages 391397. Springer, 2007. (pdf,
arXiv)
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,
doi).

Representing and reasoning with operational semantics, by Dale
Miller. Invited speaker. 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,
HAL,
doi).
© ACM, 2005.
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.
(pdf,
doi).
Errata: In the last displayed formula of Section 6, the occurrence of
r should be replaced by s_{2} (found by G. Nadathur).

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 that
appeared 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).

An 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, 2004.
(ps,
dvi,
pdf).
2003

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, pp 1829.

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).
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,
doi).
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, Roberto
Gorrieri, Alberto MarchettiSpaccamela, and Peter Wegner, Vol. 31,
September 1999.
(dvi,
PostScript,
pdf,
doi).
1998

HigherOrder Logic Programming, by Gopalan Nadathur and Dale
Miller. In Volume 5 of the Handbook of Logics for Artificial
Intelligence and Logic Programming, edited by Dov M. Gabbay,
C. J. Hogger, and J. A. Robinson (Clarendon Press, Oxford),
pp. 499590 (1998). (dvi, pdf).
1997

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
in Computational Logic, edited by U. Berger and H. Schwichtenberg.
NATO Advanced Science Institute Series, subseries F: Computer and
Systems Sciences, Springer, 399  444. Based on lectures given at
the International Summer School Marktoberdorf on Logic of Computation,
29 July  10 August 1997.
(pdf)

Logic Programming and MetaLogic in The Logic of
Computation, edited by H. Schwichtenberg. NATO Advanced Science
Institute Series, subseries F: Computer & Systems Sciences,
published by SpringerVerlag, pp. 265  308 (1997). Based on
lectures given at the International Summer School Marktoberdorf on
Logic of Computation, 25 July  6 August 1995.
(pdf)
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)
(doi).
(dvi,
pdf,
PostScript).

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. (doi).
Local copy.
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.
LICS 1994: Proceedings of the 1994 Symposium on Logics in Computer Science,
edited by S. Abramsky, pp. 272281 (pdf).
Selected in 2014 for
a TestofTime Award.
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).
1992

Unification under a mixed prefix, by Dale Miller.
Journal of Symbolic Computation, Vol. 14 (1992), 321358.
(dvi, pdf).

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).

From Operational Semantics to Abstract Machines by John Hannan
and Dale Miller.
Journal of Mathematical Structures in Computer Science,
Vol. 2, No. 4 (1992), 415459 (pdf,
doi).
1991

Logic Programming in a Fragment of Intuitionistic Linear Logic: Extended Abstract,
by Joshua Hodas and Dale Miller. LICS 1991: Sixth Annual Symposium on
Logic in Computer Science, ed. G. Kahn, pp. 3242.
(pdf,
TR).
Selected in 2011 for
a TestofTime
Award.

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).

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).
A version of this paper is available as a UPenn technical
report MSCIS9054,
August 1990 (pdf) and was published in
Extensions of Logic Programming edited by LarsHenrik Eriksson,
Lars Hallnäs, and Peter SchroederHeister,
Springer, LNAI 475, pp. 153281.

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.
1990

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).
University of Pennsylvania technical report MSCIS9059.

From operational semantics to abstract machines: Preliminary
results by John Hannan and Dale Miller in the Proceedings of
Lisp and Functional Programming, 1990.
(pdf,
doi).
University of Pennsylvania technical
report MSCIS9021.

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, pdf).

Higherorder Horn Clauses, by Gopalan Nadathur and Dale Miller,
Journal of the ACM, Vol. 37, No. 4 (1990), 777814.
(dvi,
pdf,
doi,
MathReview).

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).
Nadathur and Southern have written
a short report that
provides a counterexample to our claim that our encoding is faithful.

Abstractions in logic programming, by Dale Miller.
Logic and Computer Science, edited by Peirgiorgio Odifreddi,
Academic Press, pp. 329  359, 1990.
(dvi, 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 MetaLogic for Functional Programming, by John Hannan and
Dale Miller. A chapter in the book MetaProgramming in Logic
Programming edited by H. Abramson and M. Rogers, pp. 453476.
MIT Press, 1989. (ps,
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)

Enriching a metalanguage with higherorder features,
by John Hannan and Dale Miller. University of Pennsylvania technical
report MSCIS8845,
June 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.
(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.

Proof explanation and revision,
by Amy Felty and Dale Miller.
Technical
Report MSCIS8817,
University of Pennsylvania (1987). (pdf)

Hereditary Harrop formulas and logic programming by Dale Miller.
Proceedings of the VIII International Congress of Logic, Methodology,
and Philosophy of Science, Moscow, pp. 153156, August 1987.

A Compact Representation of Proofs, by Dale Miller.
Studia Logica, Volume 46, Number 4, pp. 347370, 1987.
(Postscript,
dvi,
pdf,
doi)

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,
doi).

Higherorder logic programming, by Dale Miller and Gopalan Nadathur.
Third International Conference on Logic Programming (ICLP), edited
by E. Shapiro, London, June 1986, 448462. LNCS 225.
(doi,
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)

Expansion tree proofs and their conversion to natural deduction
proofs by Dale Miller. In 7th Conference on Automated
Deduction, edited by R. E. Shostak, Lecture Notes in Computer
Science, No. 170, SpringerVerlag, 1984, 375393
(pdf).

A Look at TPS by Dale A. Miller, Eve Longini Cohen, and Peter B. Andrews.
In 6th Conference on Automated Deduction, edited by Donald
W. Loveland, Lecture Notes in Computer
Science, No. 138, SpringerVerlag, 1982, 5069
(pdf).
1970's

The sum of an integer's digits: some properties by Dale
Miller. Journal
of Undergraduate Mathematics, September 1976, Volume 8,
6164. Available
on JSTOR.

Observations in Pure Mathematics, by Dale Miller, finalist
paper in
the 33rd
Westinghouse Science Talent Search, 1974 (now the Regeneron
Science Talent Search):
(dvi, pdf).

The Millin
Series. When I published my first
mathematical result as an Advanced Problem in the Fibonacci
Quarterly (Problem H237, 1974), 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,
this, and
this.
A computer generated proof of this identity is reported
here.
There is a YouTube video describing a proof.
My own proof is available.