Computation with Bounded Resources
Research Group


Computation with Bounded Resources Group,
Computational Logic Group,
Department of Computer Science


CBR goes TCS

Starting in February, Georg Moser is Chair of Theoretical Computer Science @ UIBK.
The group's new website can be found at This website will no longer be maintained.
Invited Speaker: Wormshop 2019

Georg Moser has been invited to give a talk at the Wormshop 2019 to be held in Barcelona on November 5-8.
Invitation to Shonan Village

Georg Moser has been invited to participate in a Shonan Village research seminar on Higher-Order Complexity and Its Applications taking place from October 7-10 in Kanagawa, Japan.
Proof theory for branching quantifiers: CERES and beyond

CBR has been made (a small) partner in the proof-theory project "Proof Theory for Branching Quantifiers". The project is funded by the Austrian Science Fund anheaded by Matthias Baaz.
CAGE call out

The CAGE project has been terminated on April 28, 2018. All in all it has been an enjoyable, but sometimes also very hectic ride. Thanks a lot to Cody, for bringing us in, in the first place!
New Member

Fabian Mitterwallner has joined our group on November 1. He will work with us in the CAGE project and will start his master project soonish.
David Obwaller joins CBR

David Obwaller will start his PhD at our group, beginning of December 1. He will be employed on CAGE.
Cody is visiting

Cody Roux, Draper Labs, is visiting us from November 10 till November 14. We work with Cody on the CAGE project, see here.
Georg @ Funchal, Madeira

Georg gives an invited talk on the epsilon calculus at the First International Summerschool for Proof Theory of First-Order Logic in Funchal, Madeira.
Georg and Martin @Dagstuhl

Georg and Martin have been invited to present our research in Dagstuhl in a seminar on resource bound analysis in July. See the link in the Dagstuhl page for the slides of the talks given by them.

Martin will start a permaent position at INRIA and will bugger off to their lab at the Universite Nice Sophia Antipol. Congratulations! Martin will start his new position in autumn, still we hope to see him occassionally.

Georg has been invited to present our research at FSCD in September, 2017. He will speak on "Uniform Resource Analysis by Rewriting: Strengths and Weaknesses".

The first joint international workshop on Developments in Implicit Computational complExity (DICE) and FOundational and Practical Aspects of Resource Analysis (FOPARA) will be held in Uppsala, Sweden, from April 22-23, 2017 as part of ETAPS. See the workshop's website for more information.
Special Issues of DICE 2014 and 2015

Our paper "From Jinja Bytecode to Term Rewriting: A Complexity Reflecting Transformation" (Moser, Schaper) will appear in a special issue of Information and Computation. The final version can be found on our publication page.
Helmut Veith Memorial Workshop

This workshop acts as informal meeting of logicians in computer science in Austria, where we present our latest ideas. The program gives ample time for discussion as well as skiing or other wintry activities. The idea to such a workshop (series) is due to Helmut, whom we aim to honour with it. The workshop takes place from January 31 to February 2, 2017 in the University Centre Obergurgl, Tirol, see the workshop's website for further details.
FISP Kick-Off

From November 15, till November 17, we will organise the kick-off meeting of FISP. Researchers from Paris, Vienna and Innsbruck will come together to discuss their current work on the project. Furthermore we plan to invite esteemed colleagues outside the project consortium as keynote speakers. Further details can be found at the workshop's website.
New Member

Dr. Kenji Miyamoto will join our group in November. Kenji recently received his PhD from LMU Munich with his work on program extraction from co-inductive proofs. Quite naturally, he extensively contributed to MINLOG. Kenji will join the FISP project.
Logic, Complexity and Automation

The aim of Logic, Complexity and Automation (LC&A) is to bring together researchers from different areas of mathematics and computer science who all have an interest in computational complexity. The workshop is the final meeting of the ACAT project, which will end in October. It takes place at the Obergurgl University Centre, September 5-7. Check out the dedicated website.
2-year PostDoc or 3-year PhD position available within the group

CBR has an opening for a postdoc or PhD-student. The position is funded by the ANR-FWF project "The fine structure of proof systems and their computational interpretations" (FISP for short). Applications (including CV, publication list, and two references) may be sent by email, to Informal inquiries are also welcome at the same email address.
EU funding for SC-square CSA

This coordination and support activity aims to unity the two fields satisifiablity checking and symbolic computing (SC-square for short). CBR is an associate member of this CSA.
Michael Schaper & Maria A Schett visit the Oregon Programming Languages Summer School

CBR congratulates Michael and Maria to the housing grant to visit the Oregon Programming Languages Summer School in Jun 2016.
New Paper at TACAS

Michael's, Martin's, and Georg's paper describing the newest version of TcT has been accepted at TACAS. The pre-final version will be soonish available.
Andreas is a Master now!

Andreas Kochesser defended his master thesis "Complexity of Simple Loop Programs" on December 18. Congratulations! Andreas leaves CBR for now, and moves to Israel to do voluntary work for the next two years. We wish him all the best.
FISP accepted

The bilateral project "The Fine Structure of Formal Proof Systems and their Computational Interpretations" (FISP for short) has been accepted. The project is concerned with structural proof theory. It is a cooperation project between four partners, two Austrian (Innsbruck and Vienna), and two French (both in Paris).
Paper @ POPL

Stéphane's and Georg's paper on "Complexity of Interaction" has been accepted at POPL. The final version (open access) is available in our publication archive.
termcomp 2015

Yet again, TcT has won the combined ranking of the complexity competition, see here for more details. It is interesting to note that our new implementation is not yet perfect, and that it is a lot easier to prove (worst-case) lower bounds than (worst-case) upper bounds.
Paper in Journal of Logic and Computation

The paper 'Parametrised bar recursion: A unifying framework for realizability interpretations of classical dependent choice' (Powell) has been accepted for publication in the Journal of Logic and Computation.
Paper at CiE 2015

The paper "On the Computational Content of Termination Proofs" (Moser, Powell) has been accepted for presentation at CiE this year.
Paper at ICFP'15

The paper "Analysing the Complexity of Functional Programs: Higher-Order Meets First-Order" (Avanzini et al.) will be presented at this year ICFP.
Two Papers at RDP'15

The papers "Leftmost Outermost Revisited" (Hirokawa et al.) and "Multivariate Amortised Resource Analysis for Term Rewrite Systems" (Hofmann, Moser) have been accepted at this years RDP. The works can be found on our publication page.
Maria Schett @ IBM

CBR congratulates Maria Schett to her internship at the IBM Thomas J. Watson Research Center.
TcT won a Kurt Gödel medal

In 2014, the first "FLoC Olympic Games" have been conducted during the Vienna Summer of Logic. During the games, several automatic tools competed in 14 different competitions about complexity, determinacy, satisfiablity, termination, etc. Our tool TcT competed in the termination competition and won the prize for the most powerful tool in complexity analysis of term rewrite systems.

Our workshop 2FC'14 takes place on Saturday, July 12. Starting time: 14:30. See the website for further information.
New Member

As of June 1, 2014, Alexander Maringele joins our team. Alexander works on automated reasoining and soon will provide our group with its first fully fledged automated theorem prover for predicate logic with equality.
Special Issues of DICE 2012 and 2013

Our papers "A New Order-theoretic Characterisation of the Polytime Computable Functions" (Avanzini, Eguchi, Moser) and "A Combination Framework for Complexity" (Avanzini, Moser) will appear with special issues of TCS and IC respectively. The final versions can be found on our publication page.
Two Papers at RTA-TLCA 2014

The papers "Amortised Resource Analysis and Typed Polynomial Interpretations" and "Automated Complexity Analysis Based on Context-Sensitive Rewriting", co-authored by our group, have been accepted at RTA-TLCA. The papers can be found on our publication page.
New Publication

Our publication ""KBOs, Ordinals, Subrecursive Hierarchies and All That" will appear in a special issue of the Journal of Logic and Computation entitled "Concepts and Meaning". The final versions can be found on our publication page.
Old and New Members

Martin will leave us for Bolognia to work with Ugo dal Lago on the complexity analysis of higher-order rewrite systems. His corresponding fellowship, project number J-3563 has been accepted. Congratulations! Furthermore, in October Thomas Powell will join our group.
New Publication

Our journal publication "Polynomial Path Orders" has been accepted at LMCS. The paper can also be found on our publication page.
New Publication

Our publication "The Structure of Interaction" has been accepted at CSL'13, Torino, Italy. A preprint of the paper can be soon found on our publication page.
New Project

The project ACAT aims at automated runtime complexity analysis of declarative and imperative programs via transformations; it is funded by the Austrian Science Fund (FWF) and has a duration of 3 years.
New Papers

Our papers "A Combination Framework for Complexity" and "Tyrolean Complexity Tool: Features and Usage" have been accepted at 24th RTA, Eindhoven, Netherlands. Preprints of these papers can be found on our publications page.
New Member

As of April 2013, Naohi Eguichi will visit our group till September 2014. Naohi's stay is funded by the Japanese Society for the Promotion of Science.
Collegium Logicum announcement

The next workshop about Structural Proof Theory will place on November 16 and 17 at LIX, Ecole Polytechnique, Palaiseau.
New Paper

Our paper "A New Order-theoretic Characterisation of the Polytime Computable Functions" has beed accepted at 10th APLAS, Kyoto, Japan. A preprint can be found on the publications page.
Complexity Competition

The ComplexityWiki at termination-portal has been moved to the CBR page and can now be found here.
CBR homepage

Homepage of 'Computations with Bounded Resources' is online.
News archive



University of Innsbruck
Technikerstrasse 21a, 2. OG
A-6020 Innsbruck, Austria


email: {firstname.lastname}