Lucas Franceschino

Table of Contents

About me

I'm a postdoc at Inria Paris in the Prosecco Team. Previously I was a Ph.D. student under the supervision of Jean-Pierre Talpin and David Pichardie at INRIA Rennes. My research focuses on formal verification, via both dependently typed languages (mainly F*) and abstract interpretation techniques.

After a double bachelor in mathematics and computer science in France, I graduated with the master degree "Mathematical Foundation of Computer Science" at Radboud University in the Netherlands. You can find my resume here.

I like functional programming a lot: I'm a happy user of Haskell, PureScript and OCaml, occasional Coq and Idris user, and for a few years now, an F* enthusiast! I'm also a NixOS and an Emacs user.


Verified Programming at the Intersection of Dependent Types and Static Analysis


  • Lucas Franceschino


Ph.D. Thesis, 2021. PDF document, slides and defense.

Verified Functional Programming of an Abstract Interpreter


  • Lucas Franceschino
  • David Pichardie
  • Jean-Pierre Talpin


Published at SAS 2021. Draft, demo and GitHub repo.

LIO*: Low-Level Information Flow Control with F*


  • Jean-Joseph Marty‚Ć
  • Lucas Franceschino‚Ć
  • Jean-Pierre Talpin
  • Niki Vazou


To be submitted. Draft.

Abstract interpretation as a Dijkstra monad transformer for verified programming


  • Lucas Franceschino
  • David Pichardie
  • Jean-Pierre Talpin


In submission.


  • Introduction to Java
    • insa rennes, L1
  • Functional programming in Scala
    • istic rennes, L1
  • Software engineering in Scala
    • istic rennes, L2
  • Imperative programming in Java
    • istic rennes, L3



rf air ihcsecnarf sacul

Gpg key

Side projects

Here are some side projects of mine, more on my GitHub.

JS Star

A transpiler from F* code to JavaScript, written as an F* meta-program, that can run during F* typechecking phase.

F* libs

A set of F* libraries and meta programs.

Star Combinator

A tiny parser combinator library for F*.

F* Toy Static Analyser

A toy static analyser written in F*.

F* HTTP-Server

An HTTP server written as an F* meta-program, with a Elm like engine. I wrote a todo list application example in F*, that extracts as a web application.

Nix flake F*

A nix Flake for building F*, that makes it easy to deal with multiple different F* versions, with custom patches, local sources, etc.