-
Notifications
You must be signed in to change notification settings - Fork 6
Abstracts.2019.Partiality
by Ana Bove
Constructive type theory (CTT), even if originally developed for formalising mathematics, can be been seen, and is being used, as a programming language with dependent types.
However, CTT is a theory of total functions. This clearly rules out genuine partial function. Most systems based on CTT only allow structurally recursive functions as a way to guarantee totality. These limitations are really a problem when we are faced with the task of formalising and proving correct a function that do not satisfy the requirements.
The search for methodologies to simplify the formalisation of general recursive and partial function in CTT has been the topic of many research projects. Many ideas of different nature have been developed in order to facilitate the definition of this class of functions and their subsequent proof of correctness. However, the issue of how to best formalise recursive and partial functions is far from being resolved.
In this talk we will have a look at the problem and some possible solutions, going from smarter termination checkers and well-founded recursion via an accessibility predicate, to general recusion with the help of domain predicates.