Chalmers GU This information is only available in

Ana Bove's Home Page

Since February 2010, I am an Associate Professor (Docent) in the Programming Logic group at the Logic and Types division of the Department of Computer Science and Engineering at Chalmers University of Technology and Göteborg University in Göteborg, Sweden.

Further information about my work can be grouped as follows:

Follow this link for contact information.

If you are interested, here you will find my Curriculum Vitae (updated only now and then).

Latest News

PC member of CPP 2019 and LSFA 2019.
Ana Bove, June 2011

Contact Information

Email: bove(at)chalmers(dot)se
Phone: work (46) (31) 772 10 20
Fax: work (46) (31) 772 36 63
Visiting Address: Rännvägen 6B
Room: 6116
Postal Address: Department of Computer Science and Engineering
Chalmers University of Technology
S-412 96 Göteborg

Research Interests

Since 1995 I work in Constructive Type Theory and, in particular, Martin-Löf type theory.

Constructive type theory is a very expressive programming language with dependent types. In addition, logic can be represented in type theory by identifying propositions with types and proofs with terms of the corresponding types. Therefore, we can encode in a type a complete specification, requiring logical properties from an algorithm. As a consequence, algorithms are correct by construction or can be proved correct by using the expressive power of constructive type theory. In some of my papers I use type theory to prove properties of certain algorithms or systems.

A computational limitation of type theory is that, to keep the logic consistent and type-checking decidable, only structural recursive definitions are allowed, that is, definitions in which the recursive calls must have structurally smaller arguments. In my Ph.D. thesis General Recursion in Type Theory (abstract), I present a method that allows us to write general recursive algorithms (that is, non-structurally smaller recursive algorithms) in a simple way. This method, that separates the logical and the computational parts of a definition, can be seen as a first step toward closing the existing gap between programming in a Haskell-like programming language and programming in type theory. The method can also be used in the formalisation of partial functions.

Here you can check my list of publications.


Teaching Activities


From 2010 to 2018, responsible for the course TMV027/DIT321 Finite Automata Theory and Formal Languages.

Commission of Trust

Substitute member of the IT Faculty Board at Gothenburg University

Since July 2018, substitute member of the IT Faculty Board at GU. The faculty board is the highest decision-making body within the faculty, and it is responsible for strategic planning, overall management and quality assurance of education, research and collaboration.

Member of Faculty Senate at Chalmers

Since May 2016, one of member of Chalmers Faculty senate, representing the staff at the Department of Computer Science and Engineering.

Programme Manager

Since January 2013 I am programme manager of the Computer Science (Datavetenskaplig) bachelor programme at the University of Gothenburg.
For any matter related to this activity please contact me via the email address ana(dot)bove(at)gu(dot)se.

Director of Studies

Since September 2005 I am director of studies at the undergraduate and master level at the Department of Computer Science and Engineering.
For any matter related to this activity please contact me via the email address sr(dot)cs-set(dot)cse(at)chalmers(dot)se.

Project Manager

From March 2010 to July 2013, I was the project manager of ForMath, a EU FP7 STREP FET-open project lead by Thierry Coquand.
Last modified: Thu Nov 8 17:56:28 CET 2018