I'm 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 at the University of Innsbruck.
Contact
email: mail__AT__jnagele.netPGP key
Activities
I have been involved in the following 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
 Member of the Steering Committee of the International Confluence Competition (CoCo), since 2015
 CoOrganizer of the 4th International Confluence Competition (CoCo 2015), Berlin, Germany, 2015
Projects
At Queen Mary I'm 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. It implements a method called unbounded superoptimization, which relies on a constraint solver to guarantee correctness of the transformation.
 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
Journal Articles

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
Papers in Conference Proceedings

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. © SpringerVerlag
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, 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. © SpringerVerlag
doi:10.1007/9783319630465_24 
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. © SpringerVerlag
doi:10.1007/9783319431444_18 
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. © SpringerVerlag
doi:10.1007/9783319214016_5 
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. © SpringerVerlag
doi:10.1007/9783319121543_14 
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
Thesis

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
Mechanized Proofs

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
Papers and Extended Abstracts in Workshop Proceedings

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 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
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, 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
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. 
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 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
Poster

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).
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 am delivering the module on Compilers at 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).
When not verifying software, I'm a regular social badminton player and recreational runner. I ran in and would recommend the following races: 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).