Bio of Martin Avanzini
I am a researcher at the Centre Inria d’Université Côte d’Azur within the OLAS (former FoCUS) research team.
I graduated from the University of Innsbruck, where I was a member of the Computational Logic and Computation with Bounded Resources groups. My thesis was concerned with the automated complexity analysis of rewrite sytems and supervised by Georg Moser. I spend two years at the University of Bologna, working with Ugo Dal Lago on the complexity analysis of higher-order rewrite systems.
I am an enthusiastic functional programmer, have a look at my software page.
Affiliations
- Centre Inria d’Université Côte d’Azur 2018 – now
Chargé de Recherche. - Universities of Bologna and Innsbruck 2014 – 2017
FWF (Austrian science fund) Schrödinger Fellow. - University of Innsbruck 2008 – 2014
Research Assistant.
Higher Education
- PhD Degree in Computer Science. 2013
Institute of Computer Science, University of Innsbruck, Austria. Thesis Verifying Polytime Computability Automatically, supervised by Georg Moser. - Master’s Degree in Computer Science. 2009
Institute of Computer Science, University of Innsbruck, Austria. Master Thesis Automation of Polynomial Path Orders, supervised by Georg Moser. - Bachelor’s Degree in Computer Science. 2007
Institute of Computer Science, University of Innsbruck, Austria. Bachelor Thesis Termination Analysis for Scheme using S-Expression Rewrite Systems, supervised by Nao Hirokawa and Scheme Programs with Polynomially Bounded Evaluation Length supervised by Georg Moser. - Diploma Höhere Technische Lehranstalt. 2001
Civil Engineering, Htl Trenkwalderstraße, Innsbruck, Austria.
Projects
Higher-Order Probabilistic and resource-aware Reasoning (HOPR) January, 2025 – December, 2029
Site Leader. ANR PRC Project 2024. Université de Lille (CRIStAL), INRIA (Olas), Université de Rennes (IRISA).Probabilistic Programming Semantics (PPS) January, 2020 – December, 2024
Site Leader. ANR PRC Project 2019 (project number ANR-19-CE48-0014). INRIA, IRIF, LIPN, I2M.Termination and Complexity Properties of Probabilistic Programs (TC(Pro)³) February, 2020 – December, 2024
Project member. Inria associate team. Inria Nancy Grand-Est (Moqua), Inria Sophia (OLAS), University of Innsbruck.Concurrent, Resourceful and Effectful COmputation, by Geometry of Interaction June, 2015 – June, 2020
Project member. INRIA associate team. INRIA (Focus), University of Bologna, Université Paris Cité (IRIF), Kyoto University, NII (Hasuo-Lab).Expanding Logical Ideas for Complexity Analysis (ELICA) October, 2014 – September, 2019
Project member. ANR Digital Foundations (DS0705) 2014 (project number ANR-14-CE25-0005). INRIA (Focus, Carte), Paris 6 (LIP6), Paris 7 (IRIF), Paris 13 (LIPN), Paris Paris-Est Créteil (LACL), ENS Lyon (Plume).Higher-Order Complexity Analysis of Rewrite Systems April, 2014 – May, 2017
Principle investigator. FWF Schrödinger Fellowship (project number J-3563). University of Bologna / University of Innsbruck.Improving Certifiers for Termination Proofs December, 2013 – March, 2014
Research assistant. FWF standalone project (project number P22767). University of Innsbruck.Structural and Computational Proof Theory November, 2012 – May, 2013
Research assistant. Bilateral research project between ANR and FWF (project number I608-N18). University of Innsbruck.Automated Complexity Analysis November, 2011 – October, 2012
Principal investigator. Doctoral fellowship (project number NWF-2011/2/Mip7). University of Innsbruck.Derivational Complexity Analysis October, 2008 – August, 2011
Research assistant. FWF standalone project (project number P20133). University of Innsbruck.
Awards
Proposed for the Heinz Zemanek Price. October, 2016
The Heinz Zemanek price is awarded every 3 years by the Austrian Computer Society (OCG) to young researchers for outstanding PhD dissertations. I was nominated by the University of Innsbruck for this price, and also passed the final selection (8 persons) from the OCG.Kurt Gödel Medal. August, 2014
Our Tyrolean Complexity tool was distinguished with the prestigious Kurt Gödel Medal as best tool for the complexity analysis of term rewrite systems at the FLoC Olympic Games, held during the Vienna Summer of Logic.European Summer School in Logics, Languages and Computation. August, 2008
My work received second place in Springer best paper awards.
Scientific Activities
Reviewer.
Reviewer for the Deutsche Forschungsgemeinschaft (DFG).PC member. 2023
8th International Conference on Formal Structures for Computation and Deduction (FSCD’23), Rome, Italy.PC member. 2023
19th International Workshop on Termination (WST’23), Obergurgl, Austria.PC member. 2022
12th International Workshop on Computing with Terms and Graphs (TERMGRAPH’22), Haifa, Israel.PC member. 2021
17th International Workshop on Termination (WST’21), Virtual.Organiser. 2020
21st International Workshop on Logic and Computational Complexity (LCC’20), Saarbrücken, Germany (Virtual).Invited speaker. 2019
10th International Workshop on Higher-Order Rewriting (HOR’19), Dortmund, Germany.PC member. 2019
Workshop on Developments in Implicit Computational Complexity and Foundational and Practical Aspects of Resource Analysis 2019 (DICE-FOPARA’19), Prague, Czech Republic.Guest editor. 2018
Special issue on DICE (TCS, Elsevier) (TCS DICE’18).Organiser. 2017
9th Workshop on Developments in Implicit Computational Complexity (DICE’17), Thessaloniki, Greece.PC member. 2017
17th International Workshop on Logic and Computational Complexity (LCC’17), Reykjavik, Iceland.PC member. 2014
5th Workshop on Developments in Implicit Computational Complexity (DICE’14), Grenoble, France.Invited speaker. 2013
15th International Workshop on Logic and Computational Complexity (LCC’13), Torino, Italy.Invited speaker. 2013
3rd Workshop on Proof Theory and Rewriting (PTR’13), Kanazawa, Japan.
Software Development
The following gives a short list of most important software projects that I was involved in. If not mentioned otherwise, I am (among) the main developer(s). Details can be found at my software page.
IsaFoR/CeTA: A formally verified tool for checking termination, confluence and complexity proofs. I have contributed the formalisation of dependency tuples.
EasyCrypt: Game-based cryptographic proof assistant.
Expected Cost Analysis for Imperative Programs (eco-imp): Expected Cost Analysis for Imperative Programs.
GUBS: A constraint solver for polynomial inequalities.
Higher Order Complexity Analysis (HOCA): Frontend for analysing the runtime complexity of OCaml programs through first-order tools.
Higher Order Sized-Type Analysis (HOSA): Complexity analyser of higher-order programs through sized-type analysis and program instrumentation.
Implicit Computational Complexity Tool (ICCT): Analyses the complexity of functions defined through rewrite systems.
Tyrolean Complexity Tool (TCT): Full-fledged runtime complexity analyser.