Sage is a prototype functional programming language designed to provide high-coverage checking of expressive program specifications (types). Sage allows a programmer to specify not only simple types such as "Integers" and "Strings" but also arbitrary refinements from simple ranges such as "Positive Integers" to data structures with complex invariants such as "Balanced binary search trees." In addition to featuring these predicates upon types, Sage merges the syntactic categories of types and terms, in the spirit of Pure Type Systems, to express dependent types such as that of the infamous printf function. Sage performs hybrid type checking of these specifications, proving or refuting as much as possible statically, and inserting runtime checks otherwise The current implementation is a type checker and interpreter for the Sage programming language. Any system with OCaml and GNU Make Sage currently requires the Simplify theorem prover for hybrid type checking.
Idris is an experimental language with full dependent types. Dependent types allow types to be predicated on values, meaning that some aspects of a program's behaviour can be specified precisely in the type. The language is closely related to Epigram and Agda. The aims of the project are: * To provide a platform for realistic programming with dependent types. By realistic, we mean the ability to interact with the outside world and use primitive types and operations. This includes networking, file handling, concurrency, etc. * To show that full dependent types do not mean we have to abandon the functional style we have come to know and love with languages like Haskell and OCaml. lightweight dependently typed programming means allowing the programmer full access to values in types, and letting the type checker do the hard work so you don't have to! Future plans include some more useful syntax (local definitions/where clauses being the most important), a compiler,
Keywords: Calculus of Constructions, Higher Order Logic, Typed Lambda Calculus, Equational Logic, Rewriting Logic Rewriting logic together with it's membership equational sublogic favors the use of abstract specifications. It has a flexible computation system based on conditional rewriting modulo equations, and via its initial semsntics it supports a very liberal notion of inductive definitions. Pure type systems, on the other hand, in particular the calculus of constructions, provide higher-order (dependent) types, but they are based on a fixed notion of computation, namely beta-reduction. To close this gap we investigate (OCC) an equational variant of the calculus of constructions. The formal executable specification of OCC exploits the reflective capabilities of Maude, yielding an computational efficiency that brings us closer the the goal of a unified tool for programming, specification and verification integrating equational logic, higher-order logic and dependent types.
I am a postdoctoral research fellow, interested in type theory, dependently typed functional programming, multi-stage programming, compilers and programming language design. I am now working on the Generative Programming for Embedded Systems project, in the context of the Hume programming language. Software * Idris, an experimental language with full dependent types. * Ivor, a type theory based theorem proving engine with a Haskell API. * A Supercombinator Compiler, intended as a back end for Epigram. Some other toys: * A simple functional language with a built-in theorem prover, implemented with the help of Ivor. * An implementation of the simply typed lambda calculus in Ivor, with a Haskell driver. * An SK calculus evaluator, being a small experiment in modelling partial functions in Coq.