Ana Bove

Docent, avdelningen för Computing Science, Institutionen för data- och informationsteknik.

I am an Associate Professor (Docent) at the Computing Science division of the department of Computer Science and Engineering at Chalmers university of technology and University of Gothenburg in Göteborg, Sweden.

Head of the Logic and types unit in the Computing Science division.

Länk till personlig sida
​DAT060/DIT202 Logic in computer science
TDA357/DIT621 Databases

​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.

Involved in Girls Code Club, a 3 weeks bootcamp for girls studying at gymnasium.

Sidansvarig Publicerad: on 13 apr 2022.