-
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]