Logic and Types

Computing Science

Computer Science and Engineering

President

bove

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 many of my papers, including my Ph.D. thesis <a target="_blank" rel="noopener noreferrer nofollow" href="https://www.cse.chalmers.se/~bove/phd_thesis.pdf">General Recursion in Type Theory</a>, I present methods that allows us to write general recursive algorithms (that is, non-structurally smaller recursive algorithms) in type theory.

bove_Ana_Bove (2)

bove_Ana_Bove (1)

I am currently teaching the following two courses:<ul><li>DAT060/DIT203 Logic in computer science, master course in study period 1</li><li>TDA357/DIT622 Databases, bachelor course in study period 2</li></ul>I am also involved in an initiative called <a target="_blank" rel="noopener noreferrer nofollow" href="https://www.chalmers.se/gcc">Girls Code Club (GCC)</a> that, during 3 week at the beginning of the summer, brings programming and simple data analysis to girls at gymnasium level.

Persons

Choose subject

Course syllabus for

Subject

Each academic year contains different courses

See programme page at universityadmissions.se

Educational area

Permissible substitutions of compulsory courses

To see your programme syllabus – select the academic year in which you started the programme.

[en: page.studyprogrammepage.syllabusesview.coursesdescription]

Ana Bove

Contact me