Listed below are some of the talks given by
Miller at various conferences, workshops, and schools. Additional
presentations can be found on his list of
publications when that presentation was given in support of a
conference paper presentation.
Peano Arithmetic and muMALL: Work in progress, a talk
presented at the StrIP
Kick-Off Workshop, University of Birmingham, June 7-10, 2022.
Focused proof systems, a talk presented at the
Logic Winter School at CIRM, Luminy, Marseille on 28 January 2022
longer version of this talk can be found below with the
title Focusing Gentzen's LK proof system.
- How to Explain a Counterexample, a talk presented at the
Seminar at the Institut d'histoire et de philosophie des
sciences et des techniques (IHPST) on 14 December 2021
Contexts in sequents as indexed storage,
a talk presented to
the Seventh Ticamore
Meeting during 16-17 June 2021
A proof theory for model checking, a talk presented to the
Worldwide Seminar on Logic and Semantics (OWLS) on 10 March 2021.
are available. This talk is based on
a paper co-authored
with Quentin Heath.
Focusing Gentzen's LK proof system, a talk presented to
Theory Virtual Seminar on 3 March 2021. The
and a related
paper (co-authored with Chuck
Liang) are available.
Structural Proof-Theory and Logic Programming, an invited
Tease-LP: Workshop on
Trends, Extensions, Applications and Semantics of Logic
Programming. Online meeting 28-29 May 2020. Originaly planned
to be associated with ETAPS 2020 in Dublin.
A distributed and trusted web of formal proofs, an invited
talk at the
Conference on Distributed Computing and Internet Technology,
9-12 January 2020, Bhubaneswar,
Formal proof and trust, a contributed talk given at the
Conference on the History and Philosophy of Computing, 28-30
October 2019, Bergamo (Italy). Slides
and a three-page abstract dated
16 July 2019.
A proof theory for model checking and arithmetic, an invited
talk given at the
Proof Theory for
Automated Deduction, Automated Deduction for Proof Theory, 24
October 2019 in Funchal, Madeira. Slides.
Programming languages based on formal structures, talk given at the
Workshop II: Programming Languages and Notations in Bertinoro,
Italy, 1-2 October 2019. This was a meeting of
the PROGRAMme ANR
project: What is a (computer) program? Historical and
philosophical perspectives. Slides of talk.
Functional programming with λ-tree syntax, talk given
Department of Computer Science and Engineering, University of
Minnesota, 19 June 2019 and at the
Research School of Computer Science, ANU, Canberra, 8 May 2019.
Slides of talk.
Applying a linear logic perspective to arithmetic, talk given at the
Tübingen Conference on Proof-Theoretic Semantics, 27-30 March 2019.
Formal proof and trust, talk given at the
meeting 9 October 2018. Slides of talk.
Focused sequent calculus proof systems, an invited talk given
Proof Theory and its Applications, 6-7 September 2018 in Ghent
Society Summer School 2018).
Linear logic as a logical framework, talk given at
SD 17: Structures and Deduction 2017.
Abstract dated 26 July 2017.
Slides of talk.
Using linear logic and proof theory to unify computational
logic, talk given
at TLLA 17: Trends
in Linear Logic and Applications.
Abstract dated 21 July 2017.
Communicating and trusting formal proofs,
talk at LIX, 23 Feb 2017. Slides.
A proof theory for model checking was presented at
Linearity 2016 in
Porto, 25 June 2016, at
LL2016: Linear Logic:
interaction, proofs and computation (7-10 November 2016, Lyon), and
LAP 2017: Logic and Applications 2017 (18-22
September 2017, Dubrovnik).
Slides. An extended abstract, written
with Quentin Heath,
is available (31 October
Reproducibility, trust, and proof checking: From Universality of
Facts to Universality of Proofs, the Dagstuhl Seminar
of Proofs 18 October 2016. Slides
Mechanized metatheory revisited,
TYPES 2016: 22nd
International Conference on Types for Proofs and Programs.
Novi Sad, Serbia, 23-26 May 2016.
On Subexponentials, Synthetic Connectives, and Multi-Level
Logic, University of Bologna, 2 February 2016
Defining the semantics of proof evidence, invited talk.
on History and Philosophy of Computing (7 August) at
the 15th Congress of Logic,
Methodology and Philosophy of Science, Helsinki, 3-8 August
I later gave a similar talk in Natal, Brazil during LSFA 2015.
There is a video of that talk.
Proof checking and logic programming. An invited talk
to PPDP 2015 -
LOPSTR 2015, Siena, 15 July 2015
Communicating and trusting formal proofs.
ETH Zurick Department of Computer Science
Colloquium Series, 20 April
Defining the semantics of proof evidence by Dale Miller.
A talk at ITU Copenhagen 11 September 2014.
Foundational Proof Certificates by Dale Miller.
An invited talk
2014:All about Proofs, Proofs for All, Vienna, 18 July 2014.
Combining Intuitionistic and Classical Logic: a proof system and
semantics. An invited talk at LATD
2014: Logic, Algebra, and Truth Degrees.
Foundational Proof Certificates: Making proof universal and permanent by Dale Miller.
An invited talk at LFMTP
2013: Logical Frameworks and Meta-Languages: Theory and
Practice, Boston, 23 September 2013:
Talks on Foundational Proof Certificates:
Slides used at the Freie
Universität Berlin on 22 February 2013.
Slides used during the CUSO Winter
School on ``Proof and Computation", 27-31 January 2013, Les
Abstracting sequent calculus proofs to get canonical proof
structures by Dale Miller. Talk given at CMU for
of Peter Andrews's Career, 5 April 2012.
(pdf). Later the same day, I
also offered a
short speech thanking Peter as my former advisor.
Towards a broad spectrum proof certificate by Dale Miller.
Talk given at McGill and CMU in Oct 2010.
Synthetic connectives and their proof theory
by Dale Miller.
Invited talk to Section C: Methodological and Philosophical Issues
of Particular Sciences Subsection C1: Logic, Mathematics and
Computer Science. 14th
International Congress of
Logic, Methodology and Philosophy of Science, Nancy, France,
19-26 July 2011 (pdf).
Sequent Calculus: overview and recent developments by
Dale Miller. Three hours of
PLS8: 8th Panhellenic
Logic Symposium, Ioannina, Greece, July 4-8, 2011.
Fixed points and proof theory by Dale Miller.
FICS 2010: 7th
Workshop on Fixed Points in Computer Science, 21-22 August
2010, Brno, Czech Republic. Slides: (pdf).
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
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 SOS specifications in logic by Dale Miller.
Slides given during talk at SOS08,
Reykjavik, Iceland, July 2008. (pdf)
Bindings, mobility of bindings, and the ∇-quantifier.
Slides of talk at CSL'04
Reasoning about proof search specifications. Slides of invited
talk at TPHOLs 2003.
Proof Search Foundations for Logic Programming. Slides of invited
lectures at WOLLIC 2003.
Wollic 2003: 10th Workshop on Logic, Language, Information and
Computation, 29 July - 1 August 2003, Ouro Preto, Minas Gerais,
Lectures on Linear Logic and Decidability of Type Checking during
Programming Languages Summer School 2002. Recorded videos of these
A Logic for Reasoning about Logic Specifications,
by Dale Miller.
Slides given at the International Summer School on Computational
Logic, Maratea, Italy, September 2000. There were four lectures:
four, and a few extra slides on the
reverse predicate specification.
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.
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.
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)
Meta-Programming in λProlog.
UKALP meeting, Edinburgh, 10 April 1991 (36 pages) (pdf).
Logic Programming Based on Higher-Order Hereditary Harrop Formulas.
Report MS-CIS-88-77, University of Pennsylvania, October 1988.
Six hours of lectures given at the Advanced School on Foundations of Logic
Programming, Alghero, Sardinia, Italy, 17 -- 23 September 1988.