Selected Talks
Listed below are the slide presentations given
by Dale
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.

A proof theory for model checking, a talk presented to the
Online
Worldwide Seminar on Logic and Semantics (OWLS) on 10 March 2021.
The slides
are available. This talk is based on
a paper coauthored
with Quentin Heath.

Focusing Gentzen's LK proof system, a talk presented to
the Proof
Theory Virtual Seminar on 3 March 2021. The
slides,
a video,
and a related
paper (coauthored with Chuck
Liang) are available.

Structural ProofTheory and Logic Programming, an invited
talk at
TeaseLP: Workshop on
Trends, Extensions, Applications and Semantics of Logic
Programming. Online meeting 2829 May 2020. Originaly planned
to be associated with ETAPS 2020 in Dublin.
Slides and
video
are available.

A distributed and trusted web of formal proofs, an invited
talk at the
16th International
Conference on Distributed Computing and Internet Technology,
912 January 2020, Bhubaneswar,
India. Slides

Formal proof and trust, a contributed talk given at the
5th International
Conference on the History and Philosophy of Computing, 2830
October 2019, Bergamo (Italy). Slides
and a threepage 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
Autumn
Workshop II: Programming Languages and Notations in Bertinoro,
Italy, 12 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
at the
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
Third
Tübingen Conference on ProofTheoretic Semantics, 2730 March 2019.
Slides of
talk. Abstract.
Full
conference proceedings.

Formal proof and trust, talk given at the
Upscale
meeting 9 October 2018. Slides of talk.

Focused sequent calculus proof systems, an invited talk given
at the
Workshop on
Proof Theory and its Applications, 67 September 2018 in Ghent
(associated with
the Proof
Society Summer School 2018).
Abstract and
slides.

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

Communicating and trusting formal proofs,
Sémin'Ouvert
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 (710 November 2016, Lyon), and
LAP 2017: Logic and Applications 2017 (1822
September 2017, Dubrovnik).
Slides. An extended abstract, written
with Quentin Heath,
is available (31 October
2016).

Reproducibility, trust, and proof checking: From Universality of
Facts to Universality of Proofs, the Dagstuhl Seminar
Universality
of Proofs 18 October 2016. Slides
and proceedings.

Mechanized metatheory revisited,
TYPES 2016: 22nd
International Conference on Types for Proofs and Programs.
Novi Sad, Serbia, 2326 May 2016.
Abstract and
slides.

On Subexponentials, Synthetic Connectives, and MultiLevel
Delimited Control,
GDRILinear
Logic, University of Bologna, 2 February 2016
(pdf).

Defining the semantics of proof evidence, invited talk.
Session
on History and Philosophy of Computing (7 August) at
the 15th Congress of Logic,
Methodology and Philosophy of Science, Helsinki, 38 August
2015 (pdf).
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
(slides).

Communicating and trusting formal proofs.
ETH Zurick Department of Computer Science
Distinguished
Colloquium Series, 20 April
2015 (slides,
video).

Defining the semantics of proof evidence by Dale Miller.
A talk at ITU Copenhagen 11 September 2014.
Slides.

Foundational Proof Certificates by Dale Miller.
An invited talk
at ∀X.Xπ
2014:All about Proofs, Proofs for All, Vienna, 18 July 2014.
Slides.

Combining Intuitionistic and Classical Logic: a proof system and
semantics. An invited talk at LATD
2014: Logic, Algebra, and Truth Degrees.
Slides.

Foundational Proof Certificates: Making proof universal and permanent by Dale Miller.
An invited talk at LFMTP
2013: Logical Frameworks and MetaLanguages: Theory and
Practice, Boston, 23 September 2013:
abstract,
slides.

Talks on Foundational Proof Certificates:
Slides used at the Freie
Universität Berlin on 22 February 2013.
Slides used during the CUSO Winter
School on ``Proof and Computation", 2731 January 2013, Les
Diablerets, Switzerland.

Abstracting sequent calculus proofs to get canonical proof
structures by Dale Miller. Talk given at CMU for
the Celebration
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.
(pdf).

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,
1926 July 2011 (pdf).

Sequent Calculus: overview and recent developments by
Dale Miller. Three hours of
lectures during
PLS8: 8th Panhellenic
Logic Symposium, Ioannina, Greece, July 48, 2011.

Fixed points and proof theory by Dale Miller.
FICS 2010: 7th
Workshop on Fixed Points in Computer Science, 2122 August
2010, Brno, Czech Republic. Slides: (pdf).

Proof and refutation in MALL as a game, by Dale Miller. Slides used during the ANRPrelude Workshop on Games,
Dialogue, and Interaction at the University of Paris VIII, 29
September 2009.

Relations: their uses in programming and computational
specifications by Dale Miller. Slides used during the Journees
du projet PEPSRelations 15  16 Dec 2008, Paris.

Formalizing 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.
Abstract
(doi).
Slides of talk at CSL'04
(pdf).

Reasoning about proof search specifications. Slides of invited
talk at TPHOLs 2003.
(pdf, dvi).

Proof Search Foundations for Logic Programming. Slides of invited
lectures at WOLLIC 2003.
Wollic 2003: 10th Workshop on Logic, Language, Information and
Computation, 29 July  1 August 2003, Ouro Preto, Minas Gerais,
(pdf)

Lectures on Linear Logic and Decidability of Type Checking during
the Oregon
Programming Languages Summer School 2002. Recorded videos of these
talks
are archived.

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:
one,
two,
three,
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.
(DVI,
pdf,
Postscript)

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

Logic in Logic Programming: Sequent Calculus, HigherOrders, and
Linear Logic. Given at the Fourth International School for
Computer Science Researchers, Acireale, Sicily, 29 June  3 July 1992
(86 pages). (pdf)

MetaProgramming in λProlog.
UKALP meeting, Edinburgh, 10 April 1991 (36 pages) (pdf).

Logic Programming Based on HigherOrder Hereditary Harrop Formulas.
Slides available
as Technical
Report MSCIS8877, 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.
(PDF).