# Talks

- July 2018: Computability Beyond Church-Turing via Choice Sequences, LICS 2018 [].
- 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].