Pierre Néron

I am currently a quantitative developer in the Strats team at Standard Chartered in Singapore.

Previously, I was 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.

Before, I was a post-doctoral fellow in the Software Language Design and Engineering project lead by Eelco Visser at TU Delft. 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 INRIA in the Deducteam team under the supervision of Gilles Dowek (INRIA) and César A. Muñoz at NASA. 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 and Google Scholar):

2016:
- SpecCert: Specifying and Verifying Hardware-based Security Enforcement with Thomas Letan, Pierre Chifflier, Guillaume Hiet and Benjamin Morin accepted at the International Symposium on Formal Methods FM 2016
- Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics with Casper Bach Poulsen, Andrew Tolmach, and Eelco Visser, European Conference on Object-Oriented Programming ECOOP 2016
- Axiomatizing Analog Algorithms with Olivier Bournez, and Nachum Dershowitz, Computability in Europe CIE 2016 Best Paper Award
- A Constraint Language for Static Semantic Analysis based on Scope Graphs with Hendrik van Antwerpen, Andrew Tolmach, Eelco Visser, and Guido Wachsmuth, PEPM 2016 (and the extended technical report)
2015:
- DynSem: A DSL for Dynamic Semantics Specification with Vlad Vergu, and Eelco Visser, Rewriting Techniques and Applications RTA 2015
- A Theory of Name Resolution with Andrew Tolmach, Eelco Visser, and Guido Wachsmuth, European Symposium on Programming ESOP 2015 EAPLS Best Paper Award
- A Certifying Square Root and Division Elimination, Workshop on Numerical Software Verification NSV 2014
2014:
- A Language Designer's Workbench: A One-Stop-Shop for Implementation and Verification of Language Designs with Eelco Visser, Guido Wachsmuth, Andrew Tolmach, Vlad Vergu, Augusto Passalaqua, and Gabriël Konat, Onward! 2014
- Elimination of Square Roots and Divisions by Partial Inlining, Principles and Practice of Declarative Programming PPDP 2014
2013:
- A Quest for Exactness: Program Transformation for Reliable Real Numbers, PhD Thesis, with the slides of the defense
- Constrained Anti-Unification for Program Transformation with Raphaël Bost, unpublished
- A Formal Proof of Square Root and Division Elimination in Embedded Programs, Journal of Formalized Reasoning JFR (6) , extended version of the CPP 2012 paper, bibtex
- Square Root and Division Elimination in PVS, Interactive Theorem Proving ITP 2013 bibtex
2012:
- A Formal Proof of Square Root and Division Elimination in Embedded Programs, Certified Programs and Proofs CPP 2012 (extended version in JFR 2013), bibtex
2011:
- A Formal Security Model of a Smart Card Web Server with Quang-Huy Nguyen, Smart Card Research and Advanced Application Conference CARDIS 2011 , bibtex

Posters:

Poster of the Language Designer Workbench presented at SPLASH 2014
Best poster award at "Journées du GDR-GPL 2013" in Nancy, poster (in french)

Contact:
pierre.neron [at] polytechnique ( dot ) org