We employ the dependently-typed programming language Agda2 to explore formalisation of untyped and typed term graphs directly as set-based graph structures, via the gs-monoidal categories of Corradini and Gadducci, and as nested let-expressions using Pouillard and Pottier's NotSoFresh library of variable-binding abstractions.
We present an approach to develop folds for nested data types using dependent types. We call such folds $\textit{dependently typed folds}$, they have the following properties. (1) Dependently typed folds are defined by well-founded recursion and they can be defined in a total dependently typed language. (2) Dependently typed folds do not depend on maps, map functions and many terminating functions can be defined using dependently typed folds. (3) The induction principles for nested data types follow from the definitions of dependently typed folds and the programs defined by dependently typed f…
We show how the categorical logic of untyped, simply typed and dependently typed lambda calculus can be structured around the notion of category with family (cwf). To this end we introduce subcategories of simply typed cwfs (scwfs), where types do not depend on variables, and unityped cwfs (ucwfs), where there is only one type. We prove several equivalence and biequivalence theorems between cwf-based notions and basic notions of categorical logic, such as cartesian operads, Lawvere theories, categories with finite products and limits, cartesian closed categories, and locally cartesian closed c…
Felty and Miller have described what they claim to be a faithful encoding of the dependently typed lambda calculus LF in the logic of hereditary Harrop formulas, a sublogic of an intuitionistic variant of Church's Simple Theory of Types. Their encoding is based roughly on translating object expressions in LF into terms in a simply typed lambda calculus by erasing dependencies in typing and then recapturing the erased dependencies through the use of predicates. Unfortunately, this idea does not quite work. In particular, we provide a counterexample to the claim that the described encoding is fa…
We present a Coq formalisation of the small-step operational semantics of Jafun, a small Java-like language with classes. This format of semantics makes it possible to naturally specify and prove invariants that should hold at each computation step. In contrast to the Featherweight Java approach the semantics explicitly manipulates frame stack of method calls. Thanks to that one can express properties of computation that depend on execution of particular methods. On the basis of the semantics, we developed a type system that makes it possible to delineate a notion of a compound value and class…
Dependent types provide a lightweight and modular means to integrate programming and formal program verification. In particular, the types of programs written in dependently typed programming languages (Agda, Idris, F*, etc.) can be used to express specifications of program correctness. These specifications can vary from being as simple as requiring the divisor in the division function to be non-zero, to as complex as specifying the correctness of compilers of industrial-strength languages. Successful compilation of a program then guarantees that it satisfies its type-based specification. Whil…
First-order resolution has been used for type inference for many years, including in Hindley- Milner type inference, type-classes, and constrained data types. Dependent types are a new trend in functional languages. In this paper, we show that proof-relevant first-order resolution can play an important role in automating type inference and term synthesis for dependently typed languages. We propose a calculus that translates type inference and term synthesis problems in a dependently typed language to a logic program and a goal in the proof-relevant first-order Horn clause logic. The computed a…
Agda is a dependently-typed functional programming language, based on an extension of intuitionistic Martin-Löf type theory. We implement first order natural deduction in Agda. We use Agda's type checker to verify the correctness of natural deduction proofs, and also prove properties of natural deduction, using Agda's proof assistant functionality. This implementation corresponds to a formalisation of natural deduction in constructive type theory, and the proofs are verified by Agda to be correct (under the assumption that Agda itself is correct).
