# Talks

- February 2023: Realizing Continuity Using Stateful Computations, CSL 2023 [slides]
- August 2022: Constructing Unprejudiced Extensional Type Theories with Choices via Modalities, FSCD 2022 [slides]
- 2022: BioTT: a Family of Brouwerian Intuitionistic Theories Open to Classical Reasoning, Types 2022 [slides]
- 2021: Brouwerian Intuitionistic Realizability Theories, LC 2021 [slides]
- 2021: Open Bar - a Brouwerian Intuitionistic Logic with a Pinch of Excluded Middle, CSL 2021 [slides]
- 2018: A Verified Theorem Prover Backend Supported by a Monotonic Library, LPAR 2018 [slides]
- July 2018: Computability Beyond Church-Turing via Choice Sequences, LICS 2018 [slides]
- April 2018: Velisarios: Byzantine Fault-Tolerant Protocols Powered by Coq, ESOP 2018 [slides]
- June 2017: Bar Induction: The Good, the Bad, and the Ugly, LICS 2017 [slides]
- May 2017: Towards an Intuitionistic Type Theory, Computer Science Seminar, Heriot-Watt University [slides]
- May 2017: Proven-Correct Provers, ILIAS seminar, University of Luxembourg [slides]
- July 2016: Exercising Nuprl's Open-Endedness, ICMS 2016, Berlin, Germany [slides]
- March 2016: Deconstructing MinBFT for Security and Verifiability, GRSRD 2016, Nancy, France [slides]
- January 2016: A Nominal Exploration of Intuitionism, CPP 2016, Saint Petersburg, FL, USA [slides]
- September 2015: Coq as a Metatheory for Nuprl with Bar Induction, CCC 2015, Kochel am See, Germany [slides]
- September 2015: Formal Specification, Verification, and Implementation of Fault-Tolerant Systems using EvenML, AVoCS 2015, Edinburgh, Scotland [slides]
- September 2015: Nuprl's Inductive Logical Forms, AI4FM 2015, Edinburgh, Scotland [slides]
- December 2014: Past, Present and Future of Nuprl, hosted by Dedukti team [slides]
- November 2014: How Trustworthy Can Systems Become? Cornell Brown Bag seminar.
- September 2014: A Type Theory with Partial Equivalence Relations as Types, Cornell PRL seminar.
- July 2014: Towards a Formally Verified Proof Assistant, ITP 2014, VSL, Vienna, Austria [slides]
- June 2014: Developing correctly replicated databases using formal tools, DSN 2014, Atlanta, GA, USA [slides]
- October 2013: Building a verified proof assistant, Cornell PRL seminar.
- July 2013: Formal program optimization in Nuprl using computational equivalence and partial types, ITP 2013 [slides]
- July 2013: Programming in Nuprl, ENS, Paris [slides]
- October 2012: A Diversified and Correct-by-Construction Broadcast Service, WRiPE 2012 [slides]
- July 2012: Interfacing with Proof Assistants for Domain Specific Programming Using EventML, UITP 2012 [slides]
- October 2011: A simple consensus algorithm, Cornell PRL seminar.
- January 2010: Progress on Skalpel, CS PhD seminar [slides]
- May 2009: A preliminary version of Skalpel, SPLS [slides] This seminar was held at the University of Glasgow.
- January 2009: Type Error Slicing, CS PhD seminar [slides]
- September 2008: A complete realisability semantics for intersection types and arbitrary expansion variables, ICTAC 2008 , The Marmara, Istanbul, Turkey [slides]
- August 2008: Second year viva [slides]
- June 2008: Lambda-calculi and Church-Rosser property, CS PhD seminar [slides]
- March 2008: Reducibility proofs in the λ-calculus, ITRS'08, Torino, Italy [slides]
- August 2007: First year viva [slides]