Simon Guilloud, Sankalp Gambhir, Andrea Gilot, and Viktor Kuncak
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.
Work Experience
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 AssetMarch-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.
Developpement of a graphical interface in Java and a client-server architecture in C to drive a data acquisition system.
Teaching
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:
Carl Martinsson - Code Maintainability and Data Structures in Energy-Aware Software: An Empirical GitHub Study
(co-supervised with
Jennifer Gross)
Samuel Sverker - Energy-Aware Software Development in Operating Systems: A Thematic Analysis of OS-Level Optimization Techniques
(co-supervised with
Jennifer Gross)
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:
1DL201 Program Design and Data Structures (2024, 2025)
1DL042 Programming (2025)
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)