Epigram is a dependently typed programming language and an interactive programming environment. Epigram has got a type system which is strong enough to express the behaviour of programs, the type checker then guarantees that the program is well behaved. However, you don't have to go as far, you can write ordinary programs and refactor them into more trustworthy, formally checked deliverables -- Epigram supports a pay as you go approach to formal methods. Epigram is freely available this page provides access to downloads of version 1 as source or binaries for the major platforms along with relevant documentation. Development on version 2 is under way we hope this will considerably improve on the first, and details of its current state are available, in the form of a developers' 'blog.
Keywords: Constructive Logic, Type Theory, Category Theory, Lambda calculus, Quantum Computing, Certified Correct Programs main research interest is the application of constructive logic in Computer Science.An example of a constructive logic is Type Theory Type Theory is at the same time a programming language and a logic: propositions correspond to types and proofs to programs. Current research centers on theoretical aspects of Type Theory but also on the construction of elegant and efficient implementations of type theoretic languages. An example of this is the Epigram system, currently under development in Nottingham, which we use to develop programs which are correct by construction. Dr. Altenkirch's research covers applications of Category Theory as a formalism to concisely express abstract properties of mathematical constructions in Computer Science and the investigation of typed lambda calculi as a foundation of (functional) programming languages and Type Theory.
AgdaLight is a version of the Agda proof checker. It is much more volatile than Agda and it's main purpose is to serve as a test platform for cool new extensions that are too experimental to make it into the real system. Be warned that AgdaLight is an experimental system, features may disappear and the syntax may change without any notice. Features * Datatypes. * Definitions by pattern matching. * Implicit arguments. * First-order logic plugin. * QuickCheck plugin. * Inductive families. * Signatures and structures (+signature subtyping). * Command line interface. * Pattern completeness checking. * LaTeX compiler (great for writing papers). Not in AgdaLight * Termination checking. * Fancy emacs interface. * Module system.
I'm interested in the relative merits of ATS vs. Epigram which is a Pure Type System that seeks to unify types and terms, where ATS distinguishes the statics and dynamics of the language. What benefits and limitations do these approaches have on complexity for both developer and implementor? notes in atsVepig.txt
The goal of the Ynot project is to make programming with dependent types practical for a modern programming language. In particular, we are extending the Coq proof assistant to make it possible to write higher-order, imperative and concurrent programs (in the style of Haskell) through a shallow embedding of Hoare Type Theory (HTT). HTT provides a clean separation between pure and effectful computations, makes it possible to formally specify and reason about effects, and is fully compositional. more...
ATS is a PL with a highly expressive type system from the framework Applied Type System. Both dependent types and linear types are available in ATS. The current implementation of ATS (ATS/Anairiats) is written in ATS itself. It can be as efficient as C/C++ and supports * Functional programming. ATS uses eager call-by-value eval, it also supports lazy call-by-need evaluation. Linear types in ATS can often make FP run with high efficiency * Imperative programming. While features considered dangerous in other languages (e.g., explicit pointer arithmetic and explicit memory mgmt) are allowed in ATS, the type system of ATS is still able to guarantee that no run-time errors can occur * Concurrent programming. ATS, equipped with a multicore-safe implementation of garbage collection, can support multithreaded programming through the use of pthreads and parallel let * Modular programming. The module system of ATS is largely infuenced by that of Modula-3
Some Basics on ATS ATS consists of a static component (statics), where types are formed and reasoned about, and a dynamic component (dynamics), where programs are constructed and evaluated. Some Primitive Sorts and Constants The statics of ATS is a simply typed language. The types for terms in the statics are called sorts (so as to avoid potential confusion with the types for terms in the dynamics) and the terms in it are called static terms. We use sigma for sorts and s for static term. The primitive sorts in ATS include bool, int, prop, type, view and viewtype. There are also some primitive constants c in the statics, each of which is assigned a constant sort (or c-sort, for short) of the following form:
A Tutorial Implementation of a Dependently Typed Lambda Calculus Andres Löh, Conor McBride and Wouter Swierstra We present the type rules for a dependently-typed core calculus together with a straightforward implementation in Haskell. We explicitly highlight the changes necessary to shift from a simply-typed lambda calculus to the dependently-typed lambda calculus. We also describe how to extend our core language with data types and write several small example programs. The paper is accompanied by an executable interpreter and example code that allows immediate experimentation with the system we describe. Download Draft Paper (submitted to FI) Haskell source code (executable Haskell file containing all the code from the paper plus the interpreter; automatically generated from the paper sources) prelude.lp (prelude for the LambdaPi interpreter, containing several example programs) Instructions (how to get started with the LambdaPi interpreter)
Hume (Higher-order Unified Meta-Environment) is a strongly typed, mostly-functional language with an integrated tool set for developing, proving and assessing concurrent, safety-critical systems. Hume aims to extend the frontiers of language design for resource-limited systems, including real-time embedded and safety-critical systems, by introducing new levels of abstraction and provability.
The Haskell project was begun in order to unify "more than a dozen non-strict, purely functional programming languages". (mirror) We are rapidly approaching that many viable choices for programming with dependent types. 1. Epigram 2. ATS (successor to Dependent ML) 3. Agda (successor to Cayenne) 4. Ωmega 5. NuPrl 6. Twelf 7. Isabelle 8. Coq etc caveats * Some of the items on this list are theorem provers first and dependently-typed programming languages second. Adam Chlipala argues that this is not such a problem for Coq. * Some of these choices may not be real options for programing with dependent types. Twelf is designed for programming about programming languages, and, if I remember correctly, doesn't have parametric polymorphism because of something having to do with higher-order abstract syntax. Is it time yet to do anything about the cornucopia of options? see comments
This paper describes practical programming with types parameterized by numbers: e.g., an array type parameterized by the array's size or a modular group type Zn parameterized by the modulus. An attempt to add, for example, two integers of different moduli should result in a compile-time error with a clear error message. Number-parameterized types let the programmer capture more invariants through types and eliminate some run-time checks. Oleg shows several approaches towards encoding numbers into types and using those numbers to check list length, matching sizes for matrices or vectors. Oleg also points out connections to dependent types, phantom types, and shape-invariant programming.
Daniel Fridlender Mia Indrika March 2001 Inspired by Danvy, we describe a technique for defining, within the Hindley-Milner type system, some functions which seem to require a language with dependent types. We illustrate this by giving a general definition of zipWith for which the Haskell library provides a family of functions, each member of the family having a different type and arity. Our technique consists in introducing ad hoc codings for natural numbers which resemble numerals in lambda-calculus
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.
au:chlipala Ur introduces richer type system features into FP. Ur is functional, pure, statically-typed, and strict. Ur supports metaprogramming based on row types. Ur/Web is standard library and associated rules for parsing and optimization. Ur/Web supports construction of dynamic web applications backed by SQL databases. The signature of the standard library is such that well-typed Ur/Web programs "don't go wrong" in a very broad sense. They also may not: * Suffer from any kinds of code-injection attacks * Return invalid HTML * Contain dead intra-application links * Have mismatches between HTML forms and the fields expected by their handlers It is also possible to use metaprogramming to build significant application pieces by analysis of type structure - demo includes an ML-style functor for building an admin interface for an arbitrary SQL table. The Ur/Web compiler also produces very efficient object code that does not use gc
Ur/Web is a DSL for programming web applications backed by SQL db. It is statically-typed and purely functional. Ur is the base language, and the web-specific features of Ur/Web (mostly) come only in the form of special rules for parsing and optimization. The Ur core looks a lot like Standard ML, with a few Haskell-isms added, and kinder, gentler versions added of many features from dependently-typed languages like the logic behind Coq. The type system is much more expressive than in ML and Haskell, such that well-typed web applications cannot "go wrong," not just in handling single HTTP requests, but across their entire lifetimes of interacting with HTTP clients. Beyond that, Ur is unusual is using ideas from dependent typing to enable very effective metaprogramming, or programming with explicit analysis of type structure. Many common web application components can be built by Ur/Web functions that operate on types