Filippo Sestini
PhD student in the Functional Programming Lab, University of
Nottingham. My supervisor is Thorsten Altenkirch.
Address: Office A04, School of Computer Science, Jubilee Campus, Wollaton Rd, Nottingham, NG8 1BB, UK
Email: filippo dot sestini at nottingham dot ac dot uk
Research interests
- Univalent type theories
- Extensionality in Intensional Type Theory
- Directed type theory
- Normalization by evaluation
- Type Theory, proof assistants, formalization of mathematics
- Strongly and dependently typed functional programming
- Generic programming
Publications, drafts
- Normalization by Evaluation for Typed Weak Lambda-ReductionPost-proceedings of the 24th International Conference on Types for Proofs and Programs, 2019 (link)
- Proof-search in a context-sensitive logic for molecular biologyJournal of Logic and Computation, 2018 (link)
- Normalization by Evaluation for Typed Lambda-Calculi with Weak ConversionsMaster's thesis, 2018 (pdf)
Talks
- Naturality for free! --- The category interpretation of directed type theoryHomotopy Type Theory 2019, Pittsburgh, PA, 2019
- Towards Normalization for the Minimal Type Theory24th
International Conference on Types for Proofs and Programs, 2018
- A theorem prover for a logical calculus of molecular biology
1st Workshop on Trends in Linear Logic and Applications (TLLA), Oxford, 2017
Software
- Haskell
implementation of an
automatic theorem prover for Zsyntax
- Agda
formalization
of normalization by evaluation for a variant of Martin-Löf Type
Theory with weak explicit substitutions
- Agda
formalization
of normalization by evaluation for the weak lambda calculus
- Github page