Since spring 2024 I'm a compiler engineer at Apple. Before that I was a quantitative finance analyst at Bank of America. Earlier I was a postdoctoral research assistant in the Theory Group of the School of Electronic Engineering and Computer Science at Queen Mary University of London. Before that I was a research and teaching assistant and PhD student advised by Aart Middeldorp in the Computational Logic Group of the Department of Computer Science of the University of Innsbruck.
Contact
email: mail__AT__jnagele.netPGP key
Activities
I was involved in the following events:
 PCMember for the 4th International Workshop on Formal Methods for Blockchains (FMBC 2022), Haifa, Israel, 2022
 CoOrganizer of the 8th International Confluence Competition (CoCo 2019), Prague, Czech Republic, 2019
 PCMember for the 10th International Workshop on HigherOrder Rewriting (HOR 2019), Dortmund, Germany, 2019
 Member of the Steering Committee of the International Confluence Competition (CoCo), 2015 – 2019
Earlier events ...
 CoOrganizer of the 7th International Confluence Competition (CoCo 2018), Oxford, UK, 2018
 PCMember for the 7th International Workshop on Confluence (IWC 2018), Oxford, UK, 2018
 CoOrganizer of the 6th International Confluence Competition (CoCo 2017), Oxford, UK, 2017
 Lecturer at the 9th International School on Rewriting (ISR 2017), Eindhoven, The Netherlands, July 2017
 CoOrganizer of the 5th International Confluence Competition (CoCo 2016), Obergurgl, Austria, 2016
 CoOrganizer of the 4th International Confluence Competition (CoCo 2015), Berlin, Germany, 2015
Projects
At Queen Mary I was a member of the project Logical Approach to Code Generation and Optimization, working on a novel compiler optimization approach based on constraint solving.
During an internship at Microsoft Research in spring 2017, I worked on Alive, a tool that can prove correctness of peephole optimizations.
At the University of Innsbruck I was a member of the following projects, devising tools for automatic and certified analysis of rewrite systems:
 From Confluence to Unique Normal Forms: Certification and Complexity
 Confluence: Automation, Certification, Extensions
 Improving Certifiers for Termination Proofs
Software
 ebso is a superoptimizer for Ethereum byte code, sorg and ppltr are tools for generating peephole optimization rules from optimizations produced by ebso.
 CSI^ho is an automatic confluence prover for higherorder rewrite systems, based on CSI.
 CSI is an automatic confluence prover for firstorder rewrite systems.
 CeTA is a tool that certifies (non)confluence (or (non)termination or completion or complexity) proofs provided by automatic tools. It is built using IsaFoR, the Isabelle Formalization of Rewriting.
 CoCoWeb is a web interface that provides a single entry point to all tools that participate in the annual Confluence Competition (CoCo).
Publications

Julian Nagele
Mechanizing Confluence: Automated and Certified Analysis of First and HigherOrder Rewrite Systems
PhD thesis, University of Innsbruck, 2017.
urn:nbn:at:atubi:113305 
Aart Middeldorp, Julian Nagele, and Kiraku Shintani
CoCo 2019: report on the eighth confluence competition
International Journal on Software Tools for Technology Transfer 23(6), pp. 905 – 916, 2021.
doi:10.1007/s10009021006204 
Maria A Schett and Julian Nagele
Populating the Peephole Optimizer of a Smart Contract Compiler
In Proceedings of the 2nd Workshop on Formal Methods for Blockchains (FMBC 2020),
OpenAccess Series in Informatics 84, pp. 3:1 – 3:15, 2020. Schloss Dagstuhl
doi:10.4230/OASIcs.FMBC.2020.3 
Julian Nagele and Maria A Schett
Blockchain Superoptimizer
In Preproceedings of the 29th International Symposium on Logicbased Program Synthesis and Transformation (LOPSTR 2019),
pp. 166180, 2019.
arXiv:2005.05912
Earlier publications ...

Nao Hirokawa, Julian Nagele, Vincent van Oostrom, and Michio Oyamaguchi
Confluence by Critical Pair Analysis Revisited
In Proceedings of the 27th International Conference on Automated Deduction (CADE27),
Lecture Notes in Computer Science 11716, pp. 319 – 336, 2019. © Springer
doi:10.1007/9783030294366_19
arXiv:1905.11733 
Aart Middeldorp, Julian Nagele, and Kiraku Shintani
Confluence Competition 2019
In Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '19),
Lecture Notes in Computer Science 11429, pp. 25 – 40, 2019. Springer
doi:10.1007/9783030175023_2 
Ezio Bartocci, Dirk Beyer, Paul E. Black, Grigory Fedyukovich, Hubert
Garavel, Arnd Hartmanns, Marieke Huisman, Fabrice Kordon, Julian Nagele,
Mihaela Sighireanu, Bernhard Steffen, Martin Suda, Geoff Sutcliffe, Tjark
Weber, and Akihisa Yamada
TOOLympics 2019: An Overview of Competitions in Formal Methods
In Proceedings of the 25th International Conference on Tools and Algorithms for the Construction and Analysis of Systems (TACAS '19),
Lecture Notes in Computer Science 11429, pp. 3 – 24, 2019. Springer
doi:10.1007/9783030175023_1 
Julian Nagele
CoCo 2019 Participant: CSI^ho 0.3.2
In Proceedings of the 8th International Workshop on Confluence (IWC '19),
p. 59, 2019. 
Nao Hirokawa, Julian Nagele, and Aart Middeldorp
Cops and CoCoWeb: Infrastructure for Confluence Tools
In Proceedings of the 9th International Joint Conference on Automated Reasoning (IJCAR '18),
Lecture Notes in Artificial Intelligence 10900, pp. 346 – 353, 2018. © Springer
doi:10.1007/9783319942056_23 
Takahito Aoto, Makoto Hamana, Nao Hirokawa, Aart Middeldorp, Julian Nagele, Naoki Nishida, Kiraku Shintani, and Harald Zankl
Confluence Competition 2018
In Proceedings of the 3rd International Conference on Formal Structures for Computation and Deduction (FSCD '18),
Leibniz International Proceedings in Informatics 108, pp. 32:1 – 32:5, 2018. Schloss Dagstuhl
doi:10.4230/LIPIcs.FSCD.2018.32 
Julian Nagele
CoCo 2018 Participant: CSI^ho 0.3.2
In Proceedings of the 7th International Workshop on Confluence (IWC '18),
p. 68, 2018. 
Bertram Felgenhauer, Aart Middeldorp, Fabian Mitterwallner, and Julian Nagele
CoCo 2018 Participant: CSI 1.2.1
In Proceedings of the 7th International Workshop on Confluence (IWC '18),
p. 67, 2018. 
Julian Nagele
CoCo 2017 Participant: CSI^ho 0.3
In Proceedings of the 6th International Workshop on Confluence (IWC '17),
p. 77, 2017. 
Bertram Felgenhauer, Aart Middeldorp, and Julian Nagele
CoCo 2017 Participant: CSI 1.1
In Proceedings of the 6th International Workshop on Confluence (IWC '17),
p. 76, 2017. 
Julian Nagele, Christian Sternagel, and Thomas Sternagel
CoCo 2017 Participant: CeTA 2.31
In Proceedings of the 6th International Workshop on Confluence (IWC '17),
p. 72, 2017. 
Julian Nagele and Aart Middeldorp
CoCoWeb — A Convenient Web Interface for Confluence Tools
In Proceedings of the 6th International Workshop on Confluence (IWC '17),
pp. 39 – 43, 2017.
arXiv:1708.07876 
Nao Hirokawa, Julian Nagele, Vincent van Oostrom, and Michio Oyamaguchi
Critical Peaks Redefined — Φ⊔Ψ=⊤
In Proceedings of the 6th International Workshop on Confluence (IWC '17),
pp. 33 – 37, 2017.
arXiv:1708.07877 
Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp
CSI: New Evidence – A Progress Report
In Proceedings of the 26th International Conference on Automated Deduction (CADE26),
Lecture Notes in Artificial Intelligence 10395, pp. 385 – 397, 2017. © Springer
doi:10.1007/9783319630465_24 
Julian Nagele, Bertram Felgenhauer, and Harald Zankl
Certifying Confluence Proofs via Relative Termination and Rule Labeling
Logical Methods in Computer Science 13(2:4), pp. 1 – 27, 2017.
doi:10.23638/LMCS13(2:4)2017 
Julian Nagele, Vincent van Oostrom, and Christian Sternagel
A Short Mechanized Proof of the ChurchRosser Theorem by the Zproperty for the λβcalculus in Nominal Isabelle
In Proceedings of the 5th International Workshop on Confluence (IWC '16),
pp. 55 – 59, 2016.
arXiv:1609.03139 
Julian Nagele and Aart Middeldorp
Certification of Classical Confluence Results for LeftLinear Term Rewrite Systems
In Proceedings of the 7th International Conference on Interactive Theorem Proving (ITP '16),
Lecture Notes in Computer Science 9807, pp. 290 – 306, 2016. © Springer
doi:10.1007/9783319431444_18 
Julian Nagele
CoCo 2016 Participant: CSI^ho 0.2
In Proceedings of the 5th International Workshop on Confluence (IWC '16),
p. 85, 2016. 
Bertram Felgenhauer, Aart Middeldorp, and Julian Nagele
CoCo 2016 Participant: CSI 0.6
In Proceedings of the 5th International Workshop on Confluence (IWC '16),
p. 84, 2016. 
Julian Nagele, Christian Sternagel, and Thomas Sternagel
CoCo 2016 Participant: CeTA 2.28
In Proceedings of the 5th International Workshop on Confluence (IWC '16),
p. 78, 2016. 
Bertram Felgenhauer, Julian Nagele, Vincent van Oostrom, and Christian Sternagel
The Z Property
Archive of Formal Proofs, June 2016, Formal proof development.
afp:Rewriting_Z 
Julian Nagele
HigherOrder Confluence: Automation and Certification
Student Research Poster at the 8th International School on Rewriting (ISR '15)
August 2015 (Best Student Research Poster Award). 
Takahito Aoto, Nao Hirokawa, Julian Nagele, Naoki Nishida, and Harald Zankl
Confluence Competition 2015
In Proceedings of the 25th International Conference on Automated Deduction (CADE25),
Lecture Notes in Artificial Intelligence 9195, pp. 101 – 104, 2015. © Springer
doi:10.1007/9783319214016_5 
Julian Nagele
CoCo 2015 Participant: CSI^ho 0.1
In Proceedings of the 4th International Workshop on Confluence (IWC '15),
p. 47, 2015. 
Bertram Felgenhauer, Aart Middeldorp, Julian Nagele and Harald Zankl
CoCo 2015 Participant: CSI 0.5.1
In Proceedings of the 4th International Workshop on Confluence (IWC '15),
p. 46, 2015. 
Julian Nagele, Christian Sternagel, Thomas Sternagel,
René Thiemann, Sarah Winkler and Harald Zankl
CoCo Participant: CeTA 2.21
In Proceedings of the 4th International Workshop on Confluence (IWC '15),
p. 41, 2015. 
Julian Nagele and Harald Zankl
Certified Rule Labeling
In Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA '15),
Leibniz International Proceedings in Informatics 36, pp. 269 – 284, 2015. Schloss Dagstuhl
doi:10.4230/LIPIcs.RTA.2015.269 
Julian Nagele, Bertram Felgenhauer, and Aart Middeldorp
Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules
In Proceedings of the 26th International Conference on Rewriting Techniques and Applications (RTA '15),
Leibniz International Proceedings in Informatics 36, pp. 257 – 268, 2015. Schloss Dagstuhl
doi:10.4230/LIPIcs.RTA.2015.257 
Julian Nagele, René Thiemann, and Sarah Winkler
Certification of Nontermination Proofs Using Strategies and Nonlooping Derivations
In Proceedings of the 6th Working Conference on Verified Software: Theories, Tools, and Experiments (VSTTE '14),
Lecture Notes in Computer Science 8471, pp. 216 – 232, 2014. © Springer
doi:10.1007/9783319121543_14 
Julian Nagele and René Thiemann
Certification of Confluence Proofs using CeTA
In Proceedings of the 3rd International Workshop on Confluence (IWC '14),
pp. 19 – 23, 2014.
arXiv:1505.01337 
René Thiemann, Guillaume Allais, and Julian Nagele
On the Formalization of Termination Techniques based on Multiset Orderings
In Proceedings of the 23rd International Conference on Rewriting Techniques and Applications (RTA '12),
Leibniz International Proceedings in Informatics 15, pp. 339 – 354, 2012. Schloss Dagstuhl
doi:10.4230/LIPIcs.RTA.2012.339
Talks

8th International Confluence Competition,
TACAS '19, Prague, pdf 
Blockchain Superoptimizer,
SREPLS 11, London, pdf
Earlier Talks ...

7th International Confluence Competition,
FSCD '18, Oxford, pdf 
CoCoWeb — A Convenient Web Interface for Confluence Tools,
IWC '17, Oxford, pdf 
6th International Confluence Competition,
IWC '17, Oxford, pdf 
Analysing GHC Rewrite Rules,
AJSW 2016, Obergurgl, pdf 
5th International Confluence Competition,
IWC '16, Obergurgl, pdf  Certification of Classical Confluence Results for LeftLinear Term Rewrite Systems,
ITP '16, Nancy, pdf  Formalization of Classical Confluence of Leftlinear Term Rewriting Systems,
44th TRS meeting, Kanazawa, pdf  Automated Termination and Confluence Analysis of Rewrite Systems,
guest talk at the IBM Thomas J. Watson Research Center, New York, pdf 
4th International Confluence Competition,
IWC '15, Berlin, pdf  Certified Rule Labeling,
RTA '15, Warsaw, pdf  Improving Automatic Confluence Analysis of Rewrite Systems by Redundant Rules,
RTA '15, Warsaw, pdf  Residual Systems and Proof Terms for Formalizing Confluence Criteria,
41st TRS meeting, Sapporo, pdf
Teaching Activities
QMUL
In spring 2019 I delivered the module on Compilers at Queen Mary University of London.
ISR 2017
At the advanced track of the 9th International School on Rewriting, Vincent van Oostrom and I gave a course on commutation. You can find our material here.
UIBK
At the University of Innsbruck I was a teaching assistant for the following courses:
 Winter 2016/17: Logic  2 contact hours, course evaluation (in German)
 Winter 2015/16: Logic  2 contact hours, course evaluation (in German)
 Winter 2014/15: Logic  2 contact hours, course evaluation (in German)
 Winter 2013/14: Logic  2 contact hours, course evaluation (in German)
 Winter 2012/13: Logic  2 contact hours, course evaluation (in German)
 Winter 2011/12: Logic  2 contact hours, course evaluation (in German)
 Summer 2011: Formal Language and Automata Theory  2 contact hours, course evaluation (in German)
Supervised Bachelor Theses
I have (co)supervised the following bachelor theses at UIBK:
 Unification Algorithms in OCaml
 SAT Encodings for Sorting Networks
 Visualization of Sorting Networks
 Visualizing CTL Model Checking
Miscellaneous
I share many things with my partner Maria A Schett. For things we want to share in the future, and if you want to join in, download our list of ideas (password is the name of our hoover robot).
I'm a regular social badminton player and recreational runner. I ran in and would recommend the following races: Rock 'n' Roll Half Marathon Dublin 2019, EDP Lisbon Half Marathon 2017, Midnight Sun Run, Iceland 2014, BIG 25 Berlin 2013, Semi Marathon de Paris 2012.
My Erdös number is 5 (Nagele > Middeldorp > Avenhaus > Plaisted > Zaks > Erdös).