Selected Talks
Listed below are various slide presentations I have given at
conferences, workshops, or schools. Additional presentations can be
found on my list of publications when that
presentation was given in support of a conference paper presentation.

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.

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

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.