I am currently a formal methods expert at ANSSI, the French Network and Information Security Agency.
I am also interested in theory of programming languages, proof theory and computation models.
Previously, I was a post-doctoral fellow in the
Software Language Design and Engineering
project lead by
I was mainly working on a meta-framework to define
static and dynamic semantics of programming languages.
Before that, I was a PhD student at
team under the supervision of
César A. Muñoz
During this PhD, I defined a program transformation that removes square roots and divisions and proved the semantics preservation of this transformation.
Publications (also on DBLP ):
SpecCert: Specifying and Verifying Hardware-based Security Enforcement
and Benjamin Morin
accepted at the International Symposium on Formal Methods
Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics
Casper Bach Poulsen,
and Eelco Visser,
European Conference on Object-Oriented Programming
Axiomatizing Analog Algorithms
and Nachum Dershowitz,
Computability in Europe CIE 2016
Best Paper Award
A Constraint Language for Static Semantic Analysis based on Scope Graphs
Hendrik van Antwerpen,
and Guido Wachsmuth,
extended technical report)
pierre.neron [at] polytechnique ( dot ) org