Selected Talks

Listed below are some of the talks 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.

• Alessio before deep inference, a talk presented at the Celebration for Alessio Guglielmi, 18 September 2024 in Bath, UK (slides).
• Higher-level rules for sequent calculus, a talk presented at The Proof Society Worskhop 2024 12 September 2024, at the University of Birmingham, UK (slides).
• About Trust and Proof: An experimental and heterogeneous framework Dagstuhl Seminar 24341: Proof Representations: From Theory to Applications, 18-23 August 2024 (slides). This talk is based on my talk at Birmingham in December 2023 (see below).
• Focusing Gentzen's sequent calculus, a talk presented at Days in Logic, 1-3 February 2024, at the Technical University of Lisbon (slides).
• Formal Reasoning using Distributed Assertions, Distinguished Seminar, Computer Science Department, University of Birmingham, 8 December 2023 (slides).
• From axioms to synthetic inference rules via focusing, a talk presented at the Type Theory, Constructive Mathematics and Geometric Logic meeting on 4 May 2023 at CIRM, Luminy, Marseilles, France (slides).
• Combining Intuitionistic and Classical Logic: a proof system and semantics, a talk presented at the Ecumenical Logic Meeting on 2-3 March 2023 at UCL, London (slides).
• A tale of two computer scientists, a talk presented at the Logic Mentoring Workshop 2023 on 17 February 2023 in Warsaw, Poland (slides).
• Peano Arithmetic and muMALL: Work in progress, a talk based on a draft paper. Slightly different versions of this talk were given at the StrIP Kick-Off Workshop, University of Birmingham, June 7-10, 2022 (slides) and at FICS 2023, Warsaw, February 17, 2023 (slides).
• Focused proof systems, a talk presented at the Linear Logic Winter School at CIRM, Luminy, Marseille on 28 January 2022 (slides, video). A 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 PHILMATH Seminar at the Institut d'histoire et de philosophie des sciences et des techniques (IHPST) on 14 December 2021 (slides).
• Contexts in sequents as indexed storage, a talk presented to the Seventh Ticamore Meeting during 16-17 June 2021 (pdf).
• 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 co-authored 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 (co-authored with Chuck Liang) are available.
• Structural Proof-Theory and Logic Programming, an invited talk at 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. 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, 9-12 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, 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 Autumn 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 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 Proof-Theoretic Semantics, 27-30 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, 6-7 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 (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 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, 23-26 May 2016. Abstract and slides.
• On Subexponentials, Synthetic Connectives, and Multi-Level Delimited Control, GDRI-Linear 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, 3-8 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 Meta-Languages: 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", 27-31 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, 19-26 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 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 September 2009.
• 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. 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 GULP-PRODE'95: Joint Conference on Declarative Programming, Marina di Vietri (Salerno-Italy), 11-14 September 1995. (HTML, pdf, PostScript, Abstract).
• 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. Slides available as Technical 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. (PDF).