Theoretical Computer Science


TCS @ "Proof and Computation"

We have been invited to present our work on the connection between proof theory and rewriting at the yearly autumn school Proof and Computation in Herrsching, Germany. Georg will give a tutorial on "Cichon's Conjecture and other Fallacies".

It is our great pleasure to announce that our group will be present at this years PLDI, as well as FSCD. Georg will present our work on "Automated Expected Value Analysis of Recursive Programs" in Orlando, while Samuel will talk aba conversion" in Rome. Also kindly check out the alpha avoidance tool on our website.
Welcome to Jamie and Manuel!

Jamie Hochrainer and Manuel Meitinger will strengthen our group in the future. Jamie has just started her Master project on the topic of formalising of amortised cost analyses of (sophisticated) data structures, while Manuel will busy himself with (automated) cost and value analyses of probabilistic imperative programs.
Two PhD Positions in AUTOSARD available

Within the AUTOSARD project, led by Georg Moser (University of Innsbruck) and Florian Zuleger (Vienna University of Technology), both in Austria, there are two openings for 4 year PhD student positions. See vacancies for further details.
Our paper on Herbrand's Theorem and the Epsilon Calculus has been accepted.

We great pleasure we announce that Kenji and Georg's work on Herbrand's Theorem and the Epsilon Calculus with Equality has recently been accepted for publication in the Archive of Mathematical Logic. Lots of thanks go to Kenji, who worked hard on the inscrutable details of the epsilon calculus!
Inauguration Lecture

Georg will give his postponed inauguration lecture at the University of Innsbruck (together with Jan Beutel) on Wednesday, December 14 at 4pm. Kindly see here for more information. It is also possible to listen in on Zoom.
AUTOSARD has been accepted

Florian Zuleger and Georg Moser's joint national project "Automated Sublinear Amortised Resource Analysis of Data Structures (AUTOSARD)" has been accepted at the recent board meeting of the Austrian Science Fund. We will shortly commence the project that concers (expected) amortised cost analysis of data structures implemented in a strict or lazy functional setting. See here for the project's website.
4 Year PhD Position

We offer a four year PhD position in the area of Theoretical Computer Science at the earliest convenience. We are looking for a strong candidate in logic and program analysis, preferable with an interest into probabilisitic and/or quantum computing; kindly see vacancies for further details. Please apply online, until December 29, 2022.
Samuel wins Eduard-Wallnöfer Prize

Samuel Frontull has won an "Anerkennungspreis" from the Eduard-Wallnöfer-Stiftung for his work on machine translation of Ladin. Congratulations to Samuel! Ladin is a vulgar version of Latin still spoken in parts of South Tirol. Machine translations for Ladin are challenging as Ladin is a so-called 'low resource' language.
Jonas moves to Computational Logic

Jonas Schöpf has found a new home at the Computational Logic Group and will leave TCS from July 2022 onwords. Good luck Jonas for your further career!
Arnold visits!

Arnold Beckmann-- esteemed researcher in proof theory, bounded arithmetic and XAI--is visiting us next week. Arnold will also talk in the Department's lunch time seminar on Thursday, June 30 on "Hybrid AI approaches for Knowledge-Intense Manufacturing". We hope to see you all there!
CAV paper

Our paper "Automated Expected Amortised Cost Analysis of Probabilistic Data Structures" has been accepted at this years CAV! This is joint work with Lorenz Leutgeb and Florian Zuleger. We will present the paper at FloC'2022 @ Haifa.
LICS paper

Our paper "Quantum Expectation Transformers for Cost Analysis" has been accepted at LICS and will be presented this summer @ FLOC'22 in Haifa. This is joint work with Martin Avanzini, Romain Pechoux, Simon Perdix and Vladimir Zamdzhiev.
Martin visits!

Martin Avanzini, esteemed researcher at INRIA Sophia Antipolis will visit our group the upcoming week from April 11 to April 15. We'll work with him on extensions on our modular solver 'ecoimp' for probabilistic while programs.
Dani joins us to work on Jonas' Early Stage project

Danielle McKenney joins us to work on Jonas' Early Stage project as a student researcher. She will help us to develop a portofolio solver for applications of automated resource analysis tools in the context of parallel and distributed computing.
Early Stage Funding Project Accepted

The early stage funding project "An Application of Resource Analysis in Scheduling" of Jonas was accepted and has started on November the 1st with a duration of one year. Goal of this project is to investigate state-of-the-art resource analyzers and their application in scheduling. The project offers a student researcher position, recently filled with Danielle.
New Member: Samuel!

Samuel Frontull has joined our group! Samuel will study the application of machine learning for the translation of Ladin.
CAV Paper Accepted

Our Paper ATLAS: Automated Amortised Complexity Analysis of Self-Adjusting Data Structures has been accepted at CAV. The paper is joint work of Lorenz Leutgeb, Georg Moser and Florian Zuleger. Georg will give a talk about this work later this month in the Department's lunchtime seminar.
Georg Moser speaks on "Herbrand Complexity and Hilbert's Epsilon Calculus" during the PTVS on January 20.

The Proof Theory Virtual Seminar (PTVS) is a (almost) weekly seminar on proof theory and related topics; Georg will present recent work in the area of Hilbert's epsilon calculus and ancient but powerful and rarely studied method in proof theory.
SPJ gives keynote at inday students

Simon Peyton-Jones will give a keynote at the Department's inday students, reflecting on the history of Haskell and why it is good to be lazy and avoid success at all costs. The talk will be streamed on twitch; further details are forthcoming.
OOPSLA Paper accepted

Our paper A Modular Cost Analysis for Probabilistic Program has been accepted at OOPSLA and will be presented on Friday, November 20. The preprecording of Martin's talk is online at SPLASH 2020. The paper is joint work of Martin, Michael and Georg.
TermComp 2020

TermComp 2020 is over. Our tool TcT participated in five categories of the complexity competition: derivational complexity analysis (full/innermost) and runtime complexity analysis (full/innermost/innermost certified). We lost almost every category to AProVE (congrats to AProVE). But we are proud winner of the RCI certified category. Students: please join us for your Bachelor/Master projects, to help make TcT great again :-)
Michi passed his Viva!

Michael Schaper our expert on automated resource analysis of imperative programs and former head developer of TcT today passed his PhD defense with excellency. Congrats and all the best for the future! Our loss is the industry's win.
Welcome to Jonas!

Jonas Schöpf recently defended his Master thesis and startet today his first day in his PhD position. He will mainly work on average case complexity for probabilistic programs. Welcome to the crowd!
INRIA Associate Team Grant Accepted

Our Associate Team project proposal, entitled "Termination and Complexity Properties of Probabilistic Programs" has been accepted. The project, short title TC(Pro)^3, is a joint effort between partners from INRIA Nancy and Sophia Antipolis and TCS. We'll work together on questions of termination and resource analysis of probabilistic progrms, with an outlook towards application of these results in quantum computing. See our projects for more details.
Albert wins PhD Fellowship

Albert Nössig has been granted a PhD fellowship of the LFUI. Albert will work on inductive programing and concept learning. Welcome to the crowd!
Philipp defended his Master

Philipp Wirtenberger has defended his Master thesis with excellency. We wish him all the best for his future career in industry! Our loss is their gain.
Bachelor and Master Topics in TCS

The TCS group offers a number of bachelor/master projects, kindly see the corresponding teaching page. Should you wish to do a project with us, and already have some concrete ideas, simply contact us.
PhD Position available

We have an offering for a 4-year PhD position in an area of the core interests of the TCS group. In particular, we are looking for a candidate interested in one (or ideally a combination) of the following areas: (i) automation; (ii) logic and type theory; (iii) programming languages; and (iv) static program analysis. Kindly, see the information in vacancies.
TCS get's started

The homepage of the Theoretical Computer Science Group is online.