Associate Professor (Docent), Computing Science division, Department of Computer Science and Engineering.
Download my CV
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.
Published: Wed 13 Apr 2022.
Please fill in a message
Thanks! We have received your message. If you have left your email address, you will receive a response from the editor-in-chief within 2-3 working days.