Lucas Franceschino

Table of Contents

About me

I am a PhD 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, I graduated with the master degree "Mathematical Foundation of Computer Science" at Radboud University. 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.

Defense on Friday, December 10

I will defend my Ph.D. thesis on Friday, December 10 at 4 pm (Paris time, UTC+1)! You can join in person in the Métivier Room at Inria Rennes (send me an email), or join us on YouTube.


Verified Functional Programming of an Abstract Interpreter


  • Lucas Franceschino
  • David Pichardie
  • Jean-Pierre Talpin


Accepted to 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.

[Anonymized title]


  • 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.