Author

Dustin Jamner

5 papers · 2017–2025

2017peak 1 in 20172025

Frequent co-authors

Papers

showing 1–5 of 5 RSS

Theorems for free for free: parametricity, with and without types

Amal Ahmed, Dustin Jamner, Jeremy G. Siek +1 more

Artificial Intelligence · Proceedings of the ACM on Programming Languages · 29 Aug 2017 · cited 60× · DOI ↗ · more like this ·

The polymorphic blame calculus integrates static typing, including universal types, with dynamic typing. The primary challenge with this integration is preserving parametricity: even dynamically-typed code should satisfy it once it has been cast to a universal type. Ahmed et al. (2011) employ runtime type generation in the polymorphic blame calculus to preserve parametricity, but a proof that it does so has been elusive. Matthews and Ahmed (2008) gave a proof of parametricity for a closely related system that combines ML and Scheme, but later found a flaw in their proof. In this paper we present an improved version of the polymorphic blame calculus and we prove that it satisfies relational parametricity. The proof relies on a step-indexed Kripke logical relation. The step-indexing is required to make the logical relation well-defined in the case for the dynamic type. The possible worlds…

Graduality and parametricity: together again for the first time

Max S. New, Dustin Jamner, Amal Ahmed

Artificial Intelligence · Proceedings of the ACM on Programming Languages · 20 Dec 2019 · cited 36× · DOI ↗ · more like this ·

Parametric polymorphism and gradual typing have proven to be a difficult combination, with no language yet produced that satisfies the fundamental theorems of each: parametricity and graduality. Notably, Toro, Labrada, and Tanter (POPL 2019) conjecture that for any gradual extension of System F that uses dynamic type generation, graduality and parametricity are ``simply incompatible''. However, we argue that it is not graduality and parametricity that are incompatible per se, but instead that combining the syntax of System F with dynamic type generation as in previous work necessitates type-directed computation, which we show has been a common source of graduality and parametricity violations in previous work. We then show that by modifying the syntax of universal and existential types to make the type name generation explicit, we remove the need for type-directed computation, and get a…

Relational compilation for performance-critical applications: extensible proof-producing translation of functional models into low-level code

Clément Pit-Claudel, Jade Philipoom, Dustin Jamner +2 more

Artificial Intelligence · DSpace@MIT (Massachusetts Institute of Technology) · 2 Jun 2022 · cited 25× · DOI ↗ · more like this ·

There are typically two ways to compile and run a purely functional program verified using an interactive theorem prover (ITP): automatically extracting it to a similar language (typically an unverified process, like Coq to OCaml) or manually proving it equivalent to a lower-level reimplementation (like a C program). Traditionally, only the latter produced both excellent performance and end-to-end proofs.

Foundational Integration Verification of a Cryptographic Server

Andres Erbsen, Jade Philipoom, Dustin Jamner +4 more

Artificial Intelligence · Proceedings of the ACM on Programming Languages · 20 Jun 2024 · cited 7× · DOI ↗ · more like this ·

We present verification of a bare-metal server built using diverse implementation techniques and languages against a whole-system input-output specification in terms of machine code, network packets, and mathematical specifications of elliptic-curve cryptography. We used very different formal-reasoning techniques throughout the stack, ranging from computer algebra, symbolic execution, and verification-condition generation to interactive verification of functional programs including compilers for C-like and functional languages. All these component specifications and domain-specific reasoning techniques are defined and justified against common foundations in the Coq proof assistant. Connecting these components is a minimalistic specification style based on functional programs and assertions over simple objects, omnisemantics for program execution, and basic separation logic for memory…

Pyrosome: Verified Compilation for Modular Metatheory

Dustin Jamner, Gabriel Kammer, Ritam Nag +1 more

cs.PL · 8 Jul 2025 · cited 0× · arXiv ↗ · more like this ·

We present Pyrosome, a generic framework for modular language metatheory that embodies a novel approach to extensible semantics and compilation, implemented in Coq. Common techniques for semantic reasoning are often tied to the specific structures of the languages and compilers that they support. In Pyrosome, verified compilers are fully extensible, meaning that to extend a language (even with a new kind of effect) simply requires defining and verifying the compilation of the new feature, reusing the old correctness theorem for all other cases. The novel enabling idea is an inductive formulation of equivalence preservation that supports the addition of new rules to the source language, target language, and compiler. Pyrosome defines a formal, deeply embedded notion of programming languages with semantics given by dependently sorted equational theories, so all compiler-correctness proofs…