Jonathan Protzenko

According to our database1, Jonathan Protzenko authored at least 34 papers between 2013 and 2021.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Other 

Links

On csauthors.net:

Bibliography

2021
Zero-cost meta-programmed stateful functors in F.
CoRR, 2021

A modern compiler for the French tax code.
Proceedings of the CC '21: 30th ACM SIGPLAN International Conference on Compiler Construction, 2021

2020
HACL×N: Verified Generic SIMD Crypto (for all your favorite platforms).
IACR Cryptol. ePrint Arch., 2020

A Security Model and Fully Verified Implementation for the IETF QUIC Record Layer.
IACR Cryptol. ePrint Arch., 2020


HACLxN: Verified Generic SIMD Crypto (for all your favourite platforms).
Proceedings of the CCS '20: 2020 ACM SIGSAC Conference on Computer and Communications Security, 2020

2019
EverCrypt: A Fast, Verified, Cross-Platform Cryptographic Provider.
IACR Cryptol. ePrint Arch., 2019

Formally Verified Cryptographic Web Applications in WebAssembly.
IACR Cryptol. ePrint Arch., 2019

EverParse: Verified Secure Zero-Copy Parsers for Authenticated Message Formats.
Proceedings of the 28th USENIX Security Symposium, 2019

Meta-F ^\star : Proof Automation with SMT, Tactics, and Metaprograms.
Proceedings of the Programming Languages and Systems, 2019

2018
Meta-F*: Metaprogramming and Tactics in an Effectful Program Verifier.
CoRR, 2018

A monadic framework for relational verification: applied to information security, program equivalence, and optimizations.
Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

2017
Verified low-level programming embedded in F.
Proc. ACM Program. Lang., 2017

HACL*: A Verified Modern Cryptographic Library.
IACR Cryptol. ePrint Arch., 2017

A Monadic Framework for Relational Verification (Functional Pearl).
CoRR, 2017

Verified Low-Level Programming Embedded in F<sup>*</sup>.
CoRR, 2017


Dijkstra monads for free.
Proceedings of the 44th ACM SIGPLAN Symposium on Principles of Programming Languages, 2017

2016
The Design and Formalization of Mezzo, a Permission-Based Programming Language.
ACM Trans. Program. Lang. Syst., 2016

Implementing and Proving the TLS 1.3 Record Layer.
IACR Cryptol. ePrint Arch., 2016

Abstract Specifications for Weakly Consistent Data.
IEEE Data Eng. Bull., 2016

Dijkstra Monads for Free.
CoRR, 2016

Microsoft touch develop and the BBC micro: bit.
Proceedings of the 38th International Conference on Software Engineering, 2016

2015
A Few Lessons from the Mezzo Project.
Proceedings of the 1st Summit on Advances in Programming Languages, 2015

Implementing real-time collaboration in TouchDevelop using AST merges.
Proceedings of the 3rd International Workshop on Mobile Development Lifecycle, 2015

Functional Pearl: the Proof Search Monad.
Proceedings of the IWIL@LPAR 2015, 2015

Beyond Open Source: The Touch Develop Cloud-Based Integrated Development Environment.
Proceedings of the 2nd ACM International Conference on Mobile Software Engineering and Systems, 2015

Global Sequence Protocol: A Robust Abstraction for Replicated Shared State.
Proceedings of the 29th European Conference on Object-Oriented Programming, 2015

2014
Mezzo: a typed language for safe effectful concurrent programs. (Mezzo: un langage typé pour programmer de manière concurrent et sure en présence d'effets).
PhD thesis, 2014

Type Soundness and Race Freedom for Mezzo.
Proceedings of the Functional and Logic Programming - 12th International Symposium, 2014

2013
The ins and outs of iteration in Mezzo.
CoRR, 2013

The implementation of the Mezzo type-checker.
Proceedings of the 25th Symposium on Implementation and Application of Functional Languages, 2013

Programming with permissions in Mezzo.
Proceedings of the ACM SIGPLAN International Conference on Functional Programming, 2013

Illustrating the Mezzo programming language.
Proceedings of the 1st French Singaporean Workshop on Formal Methods and Applications, 2013


  Loading...