Joachim Breitner

Orcid: 0000-0003-3753-6821

Affiliations:
  • DFINITY Foundation, Switzerland
  • University of Pennsylvania, Philadelphia, PA, USA
  • Karlsruhe Institute of Technology, Karlsruhe, Germany (PhD 2016)


According to our database1, Joachim Breitner authored at least 48 papers between 2010 and 2024.

Collaborative distances:

Timeline

Legend:

Book 
In proceedings 
Article 
PhD thesis 
Dataset
Other 

Links

Online presence:

On csauthors.net:

Bibliography

2024
Bringing the WebAssembly Standard up to Speed with SpecTec.
Proc. ACM Program. Lang., 2024

2023
More Fixpoints! (Functional Pearl).
Proc. ACM Program. Lang., August, 2023

The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programming.
Proc. ACM Program. Lang., August, 2023

The curious case of the half-half Bitcoin ECDSA nonces.
IACR Cryptol. ePrint Arch., 2023

Wasm SpecTec: Engineering a Formal Language Standard.
CoRR, 2023

2021
Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code.
J. Funct. Program., 2021

2020
Explicit Renyi Entropy for Hidden Markov Models.
Proceedings of the IEEE International Symposium on Information Theory, 2020

2019
Biased Nonce Sense: Lattice Attacks against Weak ECDSA Signatures in Cryptocurrencies.
IACR Cryptol. ePrint Arch., 2019

Embracing a mechanized formalization gap.
CoRR, 2019

Demo: kaleidogen.
Proceedings of the 7th ACM SIGPLAN International Workshop on Functional Art, 2019

2018
Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report).
Proc. ACM Program. Lang., 2018

The adequacy of Launchbury's natural semantics for lazy evaluation.
J. Funct. Program., 2018

Low-deterministic security for low-nondeterministic programs.
J. Comput. Secur., 2018

More on sliding right.
IACR Cryptol. ePrint Arch., 2018

Functional Pearl: Theorem Proving for All (Equational Reasoning in Liquid Haskell).
CoRR, 2018

The sufficiently smart compiler is a theorem prover.
CoRR, 2018

Beyond correct and fast: Inspection Testing.
CoRR, 2018

Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code.
CoRR, 2018

Call Arity.
Comput. Lang. Syst. Struct., 2018

Theorem proving for all: equational reasoning in liquid Haskell (functional pearl).
Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell, 2018

Type variables in patterns.
Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell, 2018

A promise checked is a promise kept: inspection testing.
Proceedings of the 11th ACM SIGPLAN International Symposium on Haskell, 2018

Total Haskell is reasonable Coq.
Proceedings of the 7th ACM SIGPLAN International Conference on Certified Programs and Proofs, 2018

Illi Isabellistes Se Custodes Egregios Praestabant.
Proceedings of the Principled Software Development, 2018

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

Modular, higher order cardinality analysis in theory and practice.
J. Funct. Program., 2017

Sliding right into disaster: Left-to-right sliding windows leak.
IACR Cryptol. ePrint Arch., 2017

Analytic Formulas for Renyi Entropy of Hidden Markov Models.
CoRR, 2017

Lock-step simulation is child's play.
CoRR, 2017

HOLCF-Prelude.
Arch. Formal Proofs, 2017

Securing Concurrent Lazy Programs Against Information Leakage.
Proceedings of the 30th IEEE Computer Security Foundations Symposium, 2017

2016
Lazy Evaluation: From natural semantics to a machine-checked compiler transformation.
PhD thesis, 2016

Safe zero-cost coercions for Haskell.
J. Funct. Program., 2016

The meta theory of the Incredible Proof Machine.
Arch. Formal Proofs, 2016

Surprise Paradox.
Arch. Formal Proofs, 2016

On Improvements of Low-Deterministic Security.
Proceedings of the Principles of Security and Trust - 5th International Conference, 2016

The Incredible Proof Machine (Invited Talk).
Proceedings of the Eleventh Workshop on Logical Frameworks and Meta-Languages: Theory and Practice, 2016

Visual Theorem Proving with the Incredible Proof Machine.
Proceedings of the Interactive Theorem Proving - 7th International Conference, 2016

2015
The Safety of Call Arity.
Arch. Formal Proofs, 2015

Formally proving a compiler transformation safe.
Proceedings of the 8th ACM SIGPLAN Symposium on Haskell, 2015

2013
Certified HLints with Isabelle/HOLCF-Prelude.
CoRR, 2013

The Correctness of Launchbury's Natural Semantics for Lazy Evaluation.
Arch. Formal Proofs, 2013

2012
dup -- Explicit un-sharing in Haskell
CoRR, 2012

Tackling the testing migration problem with SAT-Solvers
CoRR, 2012

2011
Conditional Elimination through Code Duplication
CoRR, 2011

The General Triangle Is Unique.
Arch. Formal Proofs, 2011

2010
Shivers' Control Flow Analysis.
Arch. Formal Proofs, 2010

Free Groups.
Arch. Formal Proofs, 2010


  Loading...