default search action
Joachim Breitner
Person information
- affiliation: DFINITY Foundation, Switzerland
- affiliation: University of Pennsylvania, Philadelphia, PA, USA
- affiliation (PhD 2016): Karlsruhe Institute of Technology, Karlsruhe, Germany
Refine list
refinements active!
zoomed in on ?? of ?? records
view refined list in
export refined list as
Books and Theses
- 2016
- [b1]Joachim Breitner:
Lazy Evaluation: From natural semantics to a machine-checked compiler transformation. Karlsruhe Institute of Technology, 2016, ISBN 978-3-7315-0546-4, pp. 1-256
Journal Articles
- 2024
- [j19]Dongjun Youn, Wonho Shin, Jaehyun Lee, Sukyoung Ryu, Joachim Breitner, Philippa Gardner, Sam Lindley, Matija Pretnar, Xiaojia Rao, Conrad Watt, Andreas Rossberg:
Bringing the WebAssembly Standard up to Speed with SpecTec. Proc. ACM Program. Lang. 8(PLDI): 1559-1584 (2024) - 2023
- [j18]Lennart Augustsson, Joachim Breitner, Koen Claessen, Ranjit Jhala, Simon Peyton Jones, Olin Shivers, Guy L. Steele Jr., Tim Sweeney:
The Verse Calculus: A Core Calculus for Deterministic Functional Logic Programming. Proc. ACM Program. Lang. 7(ICFP): 417-447 (2023) - [j17]Joachim Breitner:
More Fixpoints! (Functional Pearl). Proc. ACM Program. Lang. 7(ICFP): 686-710 (2023) - 2021
- [j16]Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Joshua M. Cohen, Stephanie Weirich:
Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code. J. Funct. Program. 31: e5 (2021) - 2018
- [j15]Joachim Breitner:
Call Arity. Comput. Lang. Syst. Struct. 52: 65-91 (2018) - [j14]Simon Bischof, Joachim Breitner, Jürgen Graf, Martin Hecker, Martin Mohr, Gregor Snelting:
Low-deterministic security for low-nondeterministic programs. J. Comput. Secur. 26(3): 335-366 (2018) - [j13]Joachim Breitner:
The adequacy of Launchbury's natural semantics for lazy evaluation. J. Funct. Program. 28: e1 (2018) - [j12]Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Stephanie Weirich:
Ready, set, verify! applying hs-to-coq to real-world Haskell code (experience report). Proc. ACM Program. Lang. 2(ICFP): 89:1-89:16 (2018) - 2017
- [j11]Joachim Breitner, Brian Huffman, Neil Mitchell, Christian Sternagel:
HOLCF-Prelude. Arch. Formal Proofs 2017 (2017) - [j10]Ilya Sergey, Dimitrios Vytiniotis, Simon L. Peyton Jones, Joachim Breitner:
Modular, higher order cardinality analysis in theory and practice. J. Funct. Program. 27: e11 (2017) - [j9]Joachim Breitner, Chris Smith:
Lock-step simulation is child's play (experience report). Proc. ACM Program. Lang. 1(ICFP): 3:1-3:15 (2017) - 2016
- [j8]Joachim Breitner:
Surprise Paradox. Arch. Formal Proofs 2016 (2016) - [j7]Joachim Breitner, Denis Lohner:
The meta theory of the Incredible Proof Machine. Arch. Formal Proofs 2016 (2016) - [j6]Joachim Breitner, Richard A. Eisenberg, Simon Peyton Jones, Stephanie Weirich:
Safe zero-cost coercions for Haskell. J. Funct. Program. 26: e15 (2016) - 2015
- [j5]Joachim Breitner:
The Safety of Call Arity. Arch. Formal Proofs 2015 (2015) - 2013
- [j4]Joachim Breitner:
The Correctness of Launchbury's Natural Semantics for Lazy Evaluation. Arch. Formal Proofs 2013 (2013) - 2011
- [j3]Joachim Breitner:
The General Triangle Is Unique. Arch. Formal Proofs 2011 (2011) - 2010
- [j2]Joachim Breitner:
Free Groups. Arch. Formal Proofs 2010 (2010) - [j1]Joachim Breitner:
Shivers' Control Flow Analysis. Arch. Formal Proofs 2010 (2010)
Conference and Workshop Papers
- 2023
- [c17]Dylan Rowe, Joachim Breitner, Nadia Heninger:
The Curious Case of the Half-Half Bitcoin ECDSA Nonces. AFRICACRYPT 2023: 273-284 - 2020
- [c16]Joachim Breitner, Maciej Skorski:
Explicit Renyi Entropy for Hidden Markov Models. ISIT 2020: 2303-2308 - 2019
- [c15]Joachim Breitner, Nadia Heninger:
Biased Nonce Sense: Lattice Attacks Against Weak ECDSA Signatures in Cryptocurrencies. Financial Cryptography 2019: 3-20 - [c14]Joachim Breitner:
Demo: kaleidogen. FARM@ICFP 2019: 49-51 - 2018
- [c13]Simon Bischof, Joachim Breitner, Denis Lohner, Gregor Snelting:
Illi Isabellistes Se Custodes Egregios Praestabant. Principled Software Development 2018: 267-282 - [c12]Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, Stephanie Weirich:
Total Haskell is reasonable Coq. CPP 2018: 14-27 - [c11]Joachim Breitner:
A promise checked is a promise kept: inspection testing. Haskell@ICFP 2018: 14-25 - [c10]Richard A. Eisenberg, Joachim Breitner, Simon Peyton Jones:
Type variables in patterns. Haskell@ICFP 2018: 94-105 - [c9]Niki Vazou, Joachim Breitner, Rose Kunkel, David Van Horn, Graham Hutton:
Theorem proving for all: equational reasoning in liquid Haskell (functional pearl). Haskell@ICFP 2018: 132-144 - 2017
- [c8]Daniel J. Bernstein, Joachim Breitner, Daniel Genkin, Leon Groot Bruinderink, Nadia Heninger, Tanja Lange, Christine van Vredendaal, Yuval Yarom:
Sliding Right into Disaster: Left-to-Right Sliding Windows Leak. CHES 2017: 555-576 - [c7]Marco Vassena, Joachim Breitner, Alejandro Russo:
Securing Concurrent Lazy Programs Against Information Leakage. CSF 2017: 37-52 - 2016
- [c6]Joachim Breitner:
Visual Theorem Proving with the Incredible Proof Machine. ITP 2016: 123-139 - [c5]Joachim Breitner:
The Incredible Proof Machine (Invited Talk). LFMTP 2016: 5:1 - [c4]Joachim Breitner, Jürgen Graf, Martin Hecker, Martin Mohr, Gregor Snelting:
On Improvements of Low-Deterministic Security. POST 2016: 68-88 - 2015
- [c3]Joachim Breitner:
Formally proving a compiler transformation safe. Haskell 2015: 35-46 - 2014
- [c2]Joachim Breitner, Richard A. Eisenberg, Simon L. Peyton Jones, Stephanie Weirich:
Safe zero-cost coercions for Haskell. ICFP 2014: 189-202 - [c1]Joachim Breitner:
Call Arity. Trends in Functional Programming 2014: 34-50
Informal and Other Publications
- 2023
- [i19]Joachim Breitner, Philippa Gardner, Jaehyun Lee, Sam Lindley, Matija Pretnar, Xiaojia Rao, Andreas Rossberg, Sukyoung Ryu, Wonho Shin, Conrad Watt, Dongjun Youn:
Wasm SpecTec: Engineering a Formal Language Standard. CoRR abs/2311.07223 (2023) - [i18]Dylan Rowe, Joachim Breitner, Nadia Heninger:
The curious case of the half-half Bitcoin ECDSA nonces. IACR Cryptol. ePrint Arch. 2023: 841 (2023) - 2019
- [i17]Antal Spector-Zabusky, Joachim Breitner, Yao Li, Stephanie Weirich:
Embracing a mechanized formalization gap. CoRR abs/1910.11724 (2019) - [i16]Joachim Breitner, Nadia Heninger:
Biased Nonce Sense: Lattice Attacks against Weak ECDSA Signatures in Cryptocurrencies. IACR Cryptol. ePrint Arch. 2019: 23 (2019) - 2018
- [i15]Joachim Breitner, Antal Spector-Zabusky, Yao Li, Christine Rizkallah, John Wiegley, Stephanie Weirich:
Ready, Set, Verify! Applying hs-to-coq to real-world Haskell code. CoRR abs/1803.06960 (2018) - [i14]Joachim Breitner:
Beyond correct and fast: Inspection Testing. CoRR abs/1803.07130 (2018) - [i13]Joachim Breitner:
The sufficiently smart compiler is a theorem prover. CoRR abs/1805.08106 (2018) - [i12]Richard A. Eisenberg, Joachim Breitner, Simon Peyton Jones:
Type variables in patterns. CoRR abs/1806.03476 (2018) - [i11]Niki Vazou, Joachim Breitner, Will Kunkel, David Van Horn, Graham Hutton:
Functional Pearl: Theorem Proving for All (Equational Reasoning in Liquid Haskell). CoRR abs/1806.03541 (2018) - [i10]Joachim Breitner:
More on sliding right. IACR Cryptol. ePrint Arch. 2018: 1163 (2018) - 2017
- [i9]Joachim Breitner, Chris Smith:
Lock-step simulation is child's play. CoRR abs/1705.09704 (2017) - [i8]Joachim Breitner, Maciej Skorski:
Analytic Formulas for Renyi Entropy of Hidden Markov Models. CoRR abs/1709.09699 (2017) - [i7]Antal Spector-Zabusky, Joachim Breitner, Christine Rizkallah, Stephanie Weirich:
Total Haskell is Reasonable Coq. CoRR abs/1711.09286 (2017) - [i6]Daniel J. Bernstein, Joachim Breitner, Daniel Genkin, Leon Groot Bruinderink, Nadia Heninger, Tanja Lange, Christine van Vredendaal, Yuval Yarom:
Sliding right into disaster: Left-to-right sliding windows leak. IACR Cryptol. ePrint Arch. 2017: 627 (2017) - 2014
- [i5]Joachim Breitner:
The Correctness of Launchbury's Natural Semantics for Lazy Evaluation. CoRR abs/1405.3099 (2014) - 2013
- [i4]Joachim Breitner, Brian Huffman, Neil Mitchell, Christian Sternagel:
Certified HLints with Isabelle/HOLCF-Prelude. CoRR abs/1306.1340 (2013) - 2012
- [i3]Joachim Breitner:
Tackling the testing migration problem with SAT-Solvers. CoRR abs/1204.2974 (2012) - [i2]Joachim Breitner:
dup -- Explicit un-sharing in Haskell. CoRR abs/1207.2017 (2012) - 2011
- [i1]Joachim Breitner:
Conditional Elimination through Code Duplication. CoRR abs/1106.3478 (2011)
Coauthor Index
manage site settings
To protect your privacy, all features that rely on external API calls from your browser are turned off by default. You need to opt-in for them to become active. All settings here will be stored as cookies with your web browser. For more information see our F.A.Q.
Unpaywalled article links
Add open access links from to the list of external document links (if available).
Privacy notice: By enabling the option above, your browser will contact the API of unpaywall.org to load hyperlinks to open access articles. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Unpaywall privacy policy.
Archived links via Wayback Machine
For web page which are no longer available, try to retrieve content from the of the Internet Archive (if available).
Privacy notice: By enabling the option above, your browser will contact the API of archive.org to check for archived content of web pages that are no longer available. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Internet Archive privacy policy.
Reference lists
Add a list of references from , , and to record detail pages.
load references from crossref.org and opencitations.net
Privacy notice: By enabling the option above, your browser will contact the APIs of crossref.org, opencitations.net, and semanticscholar.org to load article reference information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the Crossref privacy policy and the OpenCitations privacy policy, as well as the AI2 Privacy Policy covering Semantic Scholar.
Citation data
Add a list of citing articles from and to record detail pages.
load citations from opencitations.net
Privacy notice: By enabling the option above, your browser will contact the API of opencitations.net and semanticscholar.org to load citation information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the OpenCitations privacy policy as well as the AI2 Privacy Policy covering Semantic Scholar.
OpenAlex data
Load additional information about publications from .
Privacy notice: By enabling the option above, your browser will contact the API of openalex.org to load additional information. Although we do not have any reason to believe that your call will be tracked, we do not have any control over how the remote server uses your data. So please proceed with care and consider checking the information given by OpenAlex.
last updated on 2024-08-03 21:14 CEST by the dblp team
all metadata released as open data under CC0 1.0 license
see also: Terms of Use | Privacy Policy | Imprint