Free Groups. - Joachim Breitner (Arch. Formal Proofs, 2010)

Shivers' Control Flow Analysis. - Joachim Breitner (Arch. Formal Proofs, 2010)

The General Triangle Is Unique. - Joachim Breitner (Arch. Formal Proofs, 2011)

Conditional Elimination through Code Duplication - Joachim Breitner (CoRR, 2011)

Tackling the testing migration problem with SAT-Solvers - Joachim Breitner (CoRR, 2012)

dup – Explicit un-sharing in Haskell - Joachim Breitner (CoRR, 2012)

The Correctness of Launchbury's Natural Semantics for Lazy Evaluation. - Joachim Breitner (Arch. Formal Proofs, 2013)

Certified HLints with Isabelle/HOLCF-Prelude. - Joachim Breitner; Brian Huffman; Neil Mitchell; Christian Sternagel (CoRR, 2013)

Formally proving a compiler transformation safe. - Joachim Breitner (Haskell, 2015)

The Safety of Call Arity. - Joachim Breitner (Arch. Formal Proofs, 2015)

Visual Theorem Proving with the Incredible Proof Machine. - Joachim Breitner (ITP, 2016)

The Incredible Proof Machine (Invited Talk). - Joachim Breitner (LFMTP, 2016)

On Improvements of Low-Deterministic Security. - Joachim Breitner; Jürgen Graf 001; Martin Hecker 001; Martin Mohr; Gregor Snelting (POST, 2016)

Surprise Paradox. - Joachim Breitner (Arch. Formal Proofs, 2016)

The meta theory of the Incredible Proof Machine. - Joachim Breitner; Denis Lohner (Arch. Formal Proofs, 2016)

Safe zero-cost coercions for Haskell. - Joachim Breitner; Richard A. Eisenberg; Simon Peyton Jones; Stephanie Weirich (J. Funct. Program., 2016)

Lazy Evaluation: From natural semantics to a machine-checked compiler transformation. - Joachim Breitner (2016)

Securing Concurrent Lazy Programs Against Information Leakage. - Marco Vassena; Joachim Breitner; Alejandro Russo (CSF, 2017)

HOLCF-Prelude. - Joachim Breitner; Brian Huffman; Neil Mitchell; Christian Sternagel (Arch. Formal Proofs, 2017)

Lock-step simulation is child's play. - Joachim Breitner; Chris Smith (CoRR, 2017)

Analytic Formulas for Renyi Entropy of Hidden Markov Models. - Joachim Breitner; Maciej Skorski (CoRR, 2017)

Sliding right into disaster: Left-to-right sliding windows leak. - Daniel J. Bernstein; Joachim Breitner; Daniel Genkin; Leon Groot Bruinderink; Nadia Heninger; Tanja Lange 001; Christine van Vredendaal; Yuval Yarom (IACR Cryptol. ePrint Arch., 2017)

Modular, higher order cardinality analysis in theory and practice. - Ilya Sergey; Dimitrios Vytiniotis; Simon L. Peyton Jones; Joachim Breitner (J. Funct. Program., 2017)

Lock-step simulation is child's play (experience report). - Joachim Breitner; Chris Smith (Proc. ACM Program. Lang., 2017)

Illi Isabellistes Se Custodes Egregios Praestabant. - Simon Bischof; Joachim Breitner; Denis Lohner; Gregor Snelting (Principled Software Development, 2018)

Total Haskell is reasonable Coq. - Antal Spector-Zabusky; Joachim Breitner; Christine Rizkallah; Stephanie Weirich (CPP, 2018)

A promise checked is a promise kept: inspection testing. - Joachim Breitner (Haskell@ICFP, 2018)

Type variables in patterns. - Richard A. Eisenberg; Joachim Breitner; Simon Peyton Jones (Haskell@ICFP, 2018)

Theorem proving for all: equational reasoning in liquid Haskell (functional pearl). - Niki Vazou; Joachim Breitner; Rose Kunkel; David Van Horn; Graham Hutton (Haskell@ICFP, 2018)

Call Arity. - Joachim Breitner (Comput. Lang. Syst. Struct., 2018)

Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code. - Joachim Breitner; Antal Spector-Zabusky; Yao Li 004; Christine Rizkallah; John Wiegley; Stephanie Weirich (CoRR, 2018)

Beyond correct and fast: Inspection Testing. - Joachim Breitner (CoRR, 2018)

The sufficiently smart compiler is a theorem prover. - Joachim Breitner (CoRR, 2018)

Functional Pearl: Theorem Proving for All (Equational Reasoning in Liquid Haskell). - Niki Vazou; Joachim Breitner; Will Kunkel; David Van Horn; Graham Hutton (CoRR, 2018)

More on sliding right. - Joachim Breitner (IACR Cryptol. ePrint Arch., 2018)

Low-deterministic security for low-nondeterministic programs. - Simon Bischof; Joachim Breitner; Jürgen Graf 001; Martin Hecker 001; Martin Mohr; Gregor Snelting (J. Comput. Secur., 2018)

The adequacy of Launchbury's natural semantics for lazy evaluation. - Joachim Breitner (J. Funct. Program., 2018)

Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report). - Joachim Breitner; Antal Spector-Zabusky; Yao Li 004; Christine Rizkallah; John Wiegley; Stephanie Weirich (Proc. ACM Program. Lang., 2018)

Demo: kaleidogen. - Joachim Breitner (FARM@ICFP, 2019)

Embracing a mechanized formalization gap. - Antal Spector-Zabusky; Joachim Breitner; Yao Li 004; Stephanie Weirich (CoRR, 2019)

Biased Nonce Sense: Lattice Attacks against Weak ECDSA Signatures in Cryptocurrencies. - Joachim Breitner; Nadia Heninger (IACR Cryptol. ePrint Arch., 2019)

Explicit Renyi Entropy for Hidden Markov Models. - Joachim Breitner; Maciej Skorski (ISIT, 2020)

Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code. - Joachim Breitner; Antal Spector-Zabusky; Yao Li 004; Christine Rizkallah; John Wiegley; Joshua M. Cohen; Stephanie Weirich (J. Funct. Program., 2021)

Wasm SpecTec: Engineering a Formal Language Standard. - Joachim Breitner; Philippa Gardner; Jaehyun Lee; Sam Lindley; Matija Pretnar; Xiaojia Rao; Andreas Rossberg; Sukyoung Ryu; Wonho Shin; Conrad Watt; Dongjun Youn (CoRR, 2023)

The curious case of the half-half Bitcoin ECDSA nonces. - Dylan Rowe; Joachim Breitner; Nadia Heninger (IACR Cryptol. ePrint Arch., 2023)

The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programming. - Lennart Augustsson; Joachim Breitner; Koen Claessen; Ranjit Jhala; Simon Peyton Jones; Olin Shivers; Guy L. Steele Jr.; Tim Sweeney (Proc. ACM Program. Lang., 2023)

More Fixpoints! (Functional Pearl). - Joachim Breitner (Proc. ACM Program. Lang., 2023)

Bringing the WebAssembly Standard up to Speed with SpecTec. - Dongjun Youn; Wonho Shin; Jaehyun Lee; Sukyoung Ryu; Joachim Breitner; Philippa Gardner; Sam Lindley; Matija Pretnar; Xiaojia Rao; Conrad Watt; Andreas Rossberg (Proc. ACM Program. Lang., 2024)