Activities

I was involved in the following events:

PC-Member for the 4th International Workshop on Formal Methods for Blockchains (FMBC 2022), Haifa, Israel, 2022
Co-Organizer of the 8th International Confluence Competition (CoCo 2019), Prague, Czech Republic, 2019
PC-Member for the 10th International Workshop on Higher-Order Rewriting (HOR 2019), Dortmund, Germany, 2019
Member of the Steering Committee of the International Confluence Competition (CoCo), 2015 – 2019

Earlier events ...

Co-Organizer of the 7th International Confluence Competition (CoCo 2018), Oxford, UK, 2018
PC-Member for the 7th International Workshop on Confluence (IWC 2018), Oxford, UK, 2018
Co-Organizer 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
Co-Organizer of the 5th International Confluence Competition (CoCo 2016), Obergurgl, Austria, 2016
Co-Organizer 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:

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 higher-order rewrite systems, based on CSI.
CSI is an automatic confluence prover for first-order 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 Higher-Order Rewrite Systems
PhD thesis, University of Innsbruck, 2017.
urn:nbn:at:at-ubi:1-13305
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/s10009-021-00620-4
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 Logic-based Program Synthesis and Transformation (LOPSTR 2019),
pp. 166-180, 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 (CADE-27),
Lecture Notes in Computer Science 11716, pp. 319 – 336, 2019. © Springer
doi:10.1007/978-3-030-29436-6_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/978-3-030-17502-3_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/978-3-030-17502-3_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/978-3-319-94205-6_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 (CADE-26),
Lecture Notes in Artificial Intelligence 10395, pp. 385 – 397, 2017. © Springer
doi:10.1007/978-3-319-63046-5_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/LMCS-13(2:4)2017
Julian Nagele, Vincent van Oostrom, and Christian Sternagel
A Short Mechanized Proof of the Church-Rosser Theorem by the Z-property 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 Left-Linear 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/978-3-319-43144-4_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
Higher-Order 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 (CADE-25),
Lecture Notes in Artificial Intelligence 9195, pp. 101 – 104, 2015. © Springer
doi:10.1007/978-3-319-21401-6_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/978-3-319-12154-3_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,
S-REPLS 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 Left-Linear Term Rewrite Systems,
ITP '16, Nancy, pdf
Formalization of Classical Confluence of Left-linear 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:

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).