Home

Welcome to my website!

I'm a Software Engineer with a PhD in Computer Science from the University of Nottingham. I'm interested in strongly typed functional programming, dependent type theory, interactive theorem proving, programming language theory and implementation, formalization of mathematics, program correctness, static analysis.

I currently work as a Functional Software Engineer at Imandra, mostly using OCaml.

I'm on Github, Linkedin, and Twitter.

Selected projects

hydrus-api (WIP): type-safe, Servant-powered Haskell bindings to Hydrus Network's Client API.
hs2agda-plugin (WIP): experimental Haskell-to-Agda transpiler as a GHC Core plugin, for lightweight formal verification of Haskell programs.
mokuro-tui, mokuro-reader: a terminal user interface (TUI) and web interface to produce and consume Japanese manga OCR data using mokuro. Written in Haskell and Javascript, respectively.
infinitary-iit-encoding: Agda formalization of a method to reduce linear infinitary inductive-inductive types to mutual inductive families, without relying on function extensionality.
setoid-universe: Agda formalization of a universe of setoids in the setoid model of intensional type theory.
nbe-mltt-wes, nbe-weak-stlc: Agda formalizations of proofs of Normalization by Evaluation for lambda calculi with weak conversion.
Zsyntax: Automated theorem prover for a linear logic-based calculus for molecular biology, written in Haskell.
Jandom: static analyser based on abstract interpretation, written in Scala.
onyx-wm: minimal tiling window manager for Mac OS, written in Haskell and Objective-C.
flight-routes: Big Data analysis of raw ADS-B data. Written in Spark for Hadoop clusters.
mu-kanren: Haskell implementation of the μKanren logic programming language.
Various Haskell implementations of toy programming languages and static analyzers: a lazy FP implementation based on graph reduction; an interpreter for a functional langauge targeting the SECD abstract machine; an interpreter and static analyzer for Plotkin's Three-Counter Machine.

Publications

T. Altenkirch, S. Boulier, A. Kaposi, C. Sattler, F. Sestini. "Constructing a universe for the setoid model". 24th International Conference on Foundations of Software Science and Computation Structures (FOSSACS), 2021. (link)
F. Sestini. "Normalization by Evaluation for Typed Weak Lambda-Reduction". Post-proceedings of the 24th International Conference on Types for Proofs and Programs (TYPES 2018), 2019. (link)
F. Sestini, S. Crafa. "Proof search in a context-sensitive logic for molecular biology", Journal of Logic and Computation, 2018. (link)

Reports

F. Sestini. "Bootstrapping Extensionality". PhD. thesis, 2023. (preliminary draft)
F. Sestini. "Normalization by Evaluation for Lambda Calculi with Weak Conversion". MSc thesis, 2018. (link)

Talks

I. Blechschmidt, M. Maggesi, F. Sestini. "How to solve your next math problem by computer. Three stories on proof‐assistants.", invited talk at the University of Padova, 2022. (webpage, flyer)
F. Sestini, T. Altenkirch. "Eliminating Infinitary Induction‐induction", contributed talk to the 27th International Conference on Types for Proofs and Programs (TYPES 2021), Online, 2021.
T. Altenkirch, S. Boulier, A. Kaposi, C. Sattler, F. Sestini. "Constructing a universe for the setoid model.", contributed talk to the 26th International Conference on Types for Proofs and Programs (TYPES 2020), Online, 2020.
F. Sestini, T. Altenkirch. "Naturality for free! - The category interpretation of directed type theory.", contributed talk to Homotopy Type Theory (HoTT 2019), Pittsburgh, 2019.
F. Sestini. "Towards Normalization for the Minimal Type Theory", contributed talk to the 24th International Conference on Types for Proofs and Programs (TYPES 2018), Braga, 2018.
F. Sestini, jww Silvia Crafa. "An automated theorem prover for a logical calculus of molecular biology", contributed talk to the Workshop on Trends in Linear Logic and Applications (TLLA), Oxford, 2017.

Latest posts

Mu-Kanren in Haskell - March 12, 2018