Abstract
We present a mechanized embedding of higher-order logic (HOL) and algebraic data types (ADTs) into first-order logic with ZFC axioms. Our approach interprets types as sets, with function (arrow) types coinciding with set-theoretic function spaces. We assume traditional FOL syntax without notation for term-level binders. To embed λ-terms, we define a notion of context, defining the closure of all abstractions occuring inside a term. We implement the embedding in the Lisa proof assistant for schematic first-order logic and its library based on axiomatic set theory (presented at ITP 2023). We show how to implement type checking and the proof steps of HOL Light as proof-producing tactics in Lisa. The embedded HOL theorems and proofs are interoperable with the existing Lisa library. This yields a form of soft type system supporting top-level polymorphism and ADTs within set theory. The approach offers tools for Lisa users to carry HOL-style proofs within set theory. It also enables the import of HOL Light theorem statements into Lisa, as well as the replay of small HOL Light kernel proofs.
Research Intern, LARA (EPFL)
July 2024
Supervised by Prof. Viktor Kuncak
Continued my Master thesis, a mechanization of inductive datatypes inside a first order logic theorem prover equipped with the axioms of set theory.
Research Intern, Digital Asset
March-August 2023
Supervised by Dr. Andreas Lochbihler
Proof formalization and mechanization of an optimization of a decentralized protocol adopted by financial institutions including Deutsche Börse, HKMA, Goldman Sachs, and BNP Paribas.
Software Intern, IOxOS Technologies
July-August 2019
Developpement of a graphical interface in Java and a client-server architecture in C to drive a data acquisition
system.
I am supervising / have supervised the following master theses:
- Mario Tannous - Specification Inference for Scala and Stainless
I am supervising / have supervised the following bachelor theses:
- Valentin Hassinen - Field Testing Stainless by Verifying Daisy’s AST Library
I have served as a Teaching Assistant for the following classes at Uppsala University:
- 1DL042 Programming (2025)
- 1DL201 Program Design and Data Structures (2024)
I have served as a Student Assistant for the following classes at EPFL:
- CS-550 Formal Verification (2022, 2023)
- CS-251 Theory of Computation (2022)
- CS-233 Introduction to Machine Learning (2021, 2022)
- EE-205 Signals and Systems (2021)
- CS-173 Digital System Design (2020)
Verified System F interepreter in Stainless
Repository
Verified typecher and interpreter for System F in Scala. The software is verified with Stainless, a verification framework for Scala.
Properties of the calculus such as progress, preservation and type derivation uniqueness are proved.
This used to be the second largest project ever verified with Stainless. It is still used as a benchmark, as part of Bolts.