Lucas Franceschino
Table of Contents
- About me
- Publications
- Teaching
- Contact
- Side projects
- footer
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.
Publications
Verified Programming at the Intersection of Dependent Types and Static Analysis
authors
- Lucas Franceschino
content
Ph.D. Thesis, 2021. PDF document, slides and defense.
Verified Functional Programming of an Abstract Interpreter
authors
- Lucas Franceschino
- David Pichardie
- Jean-Pierre Talpin
content
Published at SAS 2021. Draft, demo and GitHub repo.
LIO*: Low-Level Information Flow Control with F*
authors
- Jean-Joseph Marty†
- Lucas Franceschino†
- Jean-Pierre Talpin
- Niki Vazou
content
To be submitted. Draft.
Abstract interpretation as a Dijkstra monad transformer for verified programming
authors
- Lucas Franceschino
- David Pichardie
- Jean-Pierre Talpin
content
In submission.
Teaching
- 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
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.