Tim Sheard will give a talk in LaBRI, Tuesday, January 10th at 4pm.
Title : Nax: a logic based upon Mendler style Iteration/Recursion Combinators
Abstract : We are interested in systems which are both a sound logic and a programming language. The design of such a system is quite delicate.
Features that programmers deem absolutely necessary (rich data types, effects, unlimited recursion, possible non-termination) have negative effects on the soundness of a logic. To address these issues we have been experimenting with a language we call Nax. Nax is a simple functional language based upon a family of principled iteration/recursion combinators first described my Mendler in which every computation terminates.
Traditional logics limit the sorts of data types definable, but place no restriction on how those data types are constructed or analyzed. Following the Mendler style, we place no restriction on what sorts of data types can be defined, or on how they can be constructed, but place strict limits on how they can be analyzed. Both approaches can form the basis of a sound logic.
Careful design of Nax has led to a language which supports many features desired by programmers, including, rich datatypes (including nested dataypes, GADTS, and higher order datatypes with negative occurrences), and an expressive type inference mechanism (even in the presence of GADTS), and traditional programing style (based upon pattern matching and the writing of defining equations) while still retaining its logical properties.
