We propose a new way to reason about general recursive functional programs in the dependently typed programming language Agda, which is based on Martin-L¨of’s intuitionistic ty...
This paper is part of a line of work on using the logical techniques of polarity and focusing to design a dependent programming language, with particular emphasis on programming w...