Jonathan Protzenko

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

Collaborative distances:



In proceedings 
PhD thesis 




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

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

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

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

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

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

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

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

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