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 Computing Science 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 2017.
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 the Spring 2010 I am responsible for the course TMV027/DIT321 Finite Automata Theory and Formal Languages.

Commission of Trust

Member of Faculty Senate

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: Mon Jul 4 17:50:11 CEST 2016