Publications by Dale Miller

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

Peano Arithmetic and μMALL by Matteo Manighetti and Dale Miller. arXiv version dated 21 December 2023. The topic of this paper was presented at FICS 2023 using these slides and at TLLA-Linearity 2022 using these slides. Submitted.
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

Property-Based Testing by Elaborating Proof Outlines by Dale Miller and Alberto Momigliano. To appear in Theory and Practice of Logic Programming (TPLP). Draft dated 14 June 2024 (arXiv).

2024

About Trust and Proof: An experimental framework for heterogeneous verification by Farah Al Wardani, Kaustuv Chaudhuri, and Dale Miller. The Practice of Formal Methods: Essays in Honour of Cliff Jones, Part II, edited by A. Cavalcanti and J. Baxter. Springer LNCS 14781 (doi). Draft dated 14 May 2024.
Higher-level rules for sequent calculus (an abstract) by Dale Miller and Elaine Pimentel. To be presented at the Proof Society 2024 Workshop on Proof Theory, 9-13 September 2024, Birmingham, UK. Draft dated 19 June 2024.
Focusing Gentzen's LK proof system by Chuck Liang and Dale Miller. In Peter Schroeder-Heister on Proof-Theoretic Semantics in the Springer series Outstanding Contributions to Logic, edited by Thomas Piecha and Kai Wehmeier, February 2024. (HAL). Draft dated 28 March 2023 (first submitted April 2020). This paper proves the main metatheory results for the LKF-proof system. A recorded lecture on this paper is online. Guillaume Munch-Maccagnoni comments on this paper in the comment section of a blog post.

2023

Formal Reasoning using Distributed Assertions by Farah Al Wardani, Kaustuv Chaudhuri, and Dale Miller. 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 Jui-Hsuan Wu. CSL 2023, pp. 3:1-3:21. Draft dated 10 November 2022. (doi, hal). Slides.

2022

A Survey of the Proof-Theoretic 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), 859-904. 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 Jui-Hsuan Wu. Draft dated 2 September 2022. Presented at LFMTP 2022 (slides).
Functions-as-constructors Higher-order 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), 455-479 (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), 523-535 (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

Two applications of logic programming to Coq by Matteo Manighetti, Dale Miller, and Alberto Momigliano. Post-Proceedings for TYPES 2020, LIPIcs, Volume 188 (doi, HAL). Draft dated 29 March 2021.
Reciprocal influences between logic programming and proof theory by Dale Miller. Philosophy & Technology, 34, 75-104. Available online. (HAL, doi). Draft dated 9 April 2019.

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 Tease-LP 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.
FPC-Coq: 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 two-page abstract dated 27 April 2020. A ``work-in-progress'' 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 two-page abstract dated 7 June 2020).
On the Proof Theory of Property-Based Testing of Coinductive Specifications, or: PBT to Infinity and beyond by Roberto Blanco, Dale Miller, and Alberto Momigliano. A two-page abstract (dated 5 Feb 2020) accepted for TYPES 2020. A ``work-in-progress'' 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, 9-12 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), 857-885 (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. 625-665 (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.
Property-Based Testing via Proof Reconstruction by Roberto Blanco, Dale Miller, and Alberto Momigliano. In PPDP 2019. Draft dated 16 July 2019. (HAL, doi).
A proof-theoretic 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 post-proceedings. Draft dated 6 July 2018. (doi, HAL).
Computation-as-deduction in Abella: work in progress by Kaustuv Chaudhuri, Ulysse Gérard, and Dale Miller. Draft dated 26 May 2018. LFMTP 2018: Logical Frameworks and Meta-Languages: 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 Meta-Languages: 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

Property-Based Testing via Proof Reconstruction: Work-in-progress by Roberto Blanco, Dale Miller, and Alberto Momigliano. LFMTP 17: Logical Frameworks and Meta-Languages: 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:1-23: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. CADE-26. pages 255-273. 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 383-399. (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. 287-330 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, 7-10 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 finite-precision semantics by Ivan Gazeau, Dale Miller, and Catuscia Palamidessi. TCS 655: 92-108 (2016). doi. Draft dated 1 September 2014. Version on HAL.
Proof Certificates for Equality Reasoning by Zakaria Chihani and Dale Miller. Post-proceedings of LSFA 2015: 10th Workshop on Logical and Semantic Frameworks, with Applications. Natal, Brazil. (doi) Draft dated 25 January 2016. Version on HAL.
A multi-focused 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): 577-603). (doi). Version dated 1 December 2013: pdf.
Functions-as-constructors Higher-order Unification by Tomer Libal and Dale Miller. Proceedings of to FSCD 2016. Draft dated 15 April 2016.
Well-Typed 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. Post-proceedings of LOPSTR 2015, edited by Moreno Falaschi. LNCS 9527, pp. 3-17 (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 IWIL-2015: 11th International Workshop on the Implementation of Logics, Fiji, 23 November 2015. Draft dated 9 November 2015.
On Subexponentials, Synthetic Connectives, and Multi-Level Delimited Control by Chuck Liang and Dale Miller. The Proceedings of LPAR-20. 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 LPAR-20. 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. 150-163. Version dated 1 December 2014: pdf.
A lightweight formalization of the metatheory of bisimulation-up-to by Kaustuv Chaudhuri, Matteo Cimini, and Dale Miller. CPP 2015: Proceedings of the 2015 Conference on Certified Programs and Proofs, pp. 157-166. (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, 19-26 July 2011. Edited by P. Schroeder-Heister, W. Hodges, G. Heinzmann, and P. E. Bour, pp. 323-342. 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 Higher-Order 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 (North-Holland), pp. 215-254.

2013

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).
Checking foundational proof certificates for first-order logic (extended abstract) by Zakaria Chihani, Dale Miller, and Fabien Renaud. Proceedings of PxTP 2013: Proof Exchange for Theorem Proving, 9-10 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 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.
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. Version on HAL.
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. (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):86-111, February 2013 (doi). Draft dated 7 October 2012: pdf. Version on HAL.

2012

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 non-local 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, 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.
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.
Nominal abstraction by Andrew Gacek, Dale Miller, and Gopalan Nadathur. Information & Computation, 209 (2011), pp. 48-73. Draft dated 22 September 2010: (pdf, arXiv).

2010

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.
A framework for proof systems by Vivek Nigam and Dale Miller. Journal of Automated Reasoning, 45(2), 157-188 (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. ACM-BCS 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. 654-672 (doi, pdf).

2009

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.
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. 129-140. Also (pdf).
A Unified Sequent Calculus for Focused Proofs by Chuck Liang and Dale Miller. Proceeding of LICS 09, pp. 355-364. (pdf)

2008

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

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 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).
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 391-397. Springer, 2007. (pdf, arXiv)

2006

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, 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 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, 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 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. (pdf, doi). Errata: In the last displayed formula of Section 6, the occurrence of r should be replaced by s₂ (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. 1-5 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 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.

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 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).
An 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, 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. 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, pp 18-29.
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).

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

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 Marchetti-Spaccamela, and Peter Wegner, Vol. 31, September 1999. (dvi, PostScript, pdf, doi).

1998

Higher-Order 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. 499-590 (1998). (dvi, pdf).

1997

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 in Computational Logic, edited by U. Berger and H. Schwichtenberg. NATO Advanced Science Institute Series, sub-series 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 Meta-Logic in The Logic of Computation, edited by H. Schwichtenberg. NATO Advanced Science Institute Series, sub-series F: Computer & Systems Sciences, published by Springer-Verlag, 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 Multiple-Conclusion Specification Logic, by Dale Miller. Theoretical Computer Science 165(1): 201-232 (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):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. LICS 1994: Proceedings of the 1994 Symposium on Logics in Computer Science, edited by S. Abramsky, pp. 272-281 (pdf). Selected in 2014 for a Test-of-Time 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, Springer-Verlag, Lecture Notes in Computer Science, Vol. 798, 1994, pp. 206-221. (PostScript, pdf).

1992

Unification under a mixed prefix, by Dale Miller. Journal of Symbolic Computation, Vol. 14 (1992), 321-358. (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. Springer-Verlag, LNCS 660, pp. 242-265. (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), 415-459 (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. 32-42. (pdf, TR). Selected in 2011 for a Test-of-Time Award.
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).
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). A version of this paper is available as a UPenn technical report MS-CIS-90-54, August 1990 (pdf) and was published in Extensions of Logic Programming edited by Lars-Henrik Eriksson, Lars Hallnäs, and Peter Schroeder-Heister, Springer, LNAI 475, pp. 153-281.
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.

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 MS-CIS-90-59.
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 MS-CIS-90-21.
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, pdf).
Higher-order Horn Clauses, by Gopalan Nadathur and Dale Miller, Journal of the ACM, Vol. 37, No. 4 (1990), 777-814. (dvi, pdf, doi, MathReview).
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). 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 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 Meta-Logic for Functional Programming, by John Hannan and Dale Miller. A chapter in the book Meta-Programming in Logic Programming edited by H. Abramson and M. Rogers, pp. 453-476. 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 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)
Enriching a meta-language with higher-order features, by John Hannan and Dale Miller. University of Pennsylvania technical report MS-CIS-88-45, 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, 98-105.
Proof explanation and revision, by Amy Felty and Dale Miller. Technical Report MS-CIS-88-17, 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. 153-156, August 1987.
A Compact Representation of Proofs, by Dale Miller. Studia Logica, Volume 46, Number 4, pp. 347-370, 1987. (Postscript, dvi, pdf, doi)
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, doi).
Higher-order logic programming, by Dale Miller and Gopalan Nadathur. Third International Conference on Logic Programming (ICLP), edited by E. Shapiro, London, June 1986, 448-462. 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, 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)
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, Springer-Verlag, 1984, 375-393 (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, Springer-Verlag, 1982, 50-69 (pdf).

1970's

The sum of an integer's digits: some properties by Dale Miller. Journal of Undergraduate Mathematics, September 1976, Volume 8, 61-64. 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 H-237, 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.