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: Research Interests See also my publications Teaching Activities Management Activities Follow this link for contact information. If you are interested, here you will find my full/short Curriculum Vitae (both updated only now and then).

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 SWEDEN

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.

Some Recent Activities

• Organiser of TYPES 2011, 8-11 September 2011, Bergen, Norway
• Organiser of DTP 2011, 27 August 2011, Nijmegen, the Netherlands
• PC member of TFP 2011, 16-18 May 2011, Madrid, Spain
• PC member of MSFP 2010, 25 September 2010, Baltimore, Maryland, USA
• Organiser of PAR 2010, 15 July 2010, Edinburgh, Scottland
• Invited speaker at DTP 2010, 9-10 July 2010, Edinburgh, United Kingdom
• Invited speaker at the session dedicated to MSFP during MFPS 2009, 3-7 April 2009, Oxford, United Kingdom

Teaching Activities

Courses

From the Spring 2010 I am responsible for the course TMV026/DIT321 Finite Automata Theory and Formal Languages.

Master Proposals

If you want to make a master thesis with me follow this link master thesis.
Other proposals at the Computer science division are found here.

Management Activities

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 Management

Since March 2010 I am the project manager of ForMath, a EU FP7 STREP FET-open project lead by Thierry Coquand.