A solution to the PoplMark challenge and more.

Ott is a tool for writing definitions of programming languages and calculi. It takes as input a definition of a language syntax and semantics, in a concise and readable ASCII notation that is close to what one would write in informal mathematics. It generates LaTeX to build a typeset version of the definition, and Coq, HOL, and Isabelle versions of the definition. Additionally, it can be run as a filter, taking a LaTeX/Coq/Isabelle/HOL source file with embedded (symbolic) terms of the defined language, parsing them and replacing them by target-system terms. For a simple example, here is an Ott source file for an untyped call-by-value lambda calculus (test10.ott), and the generated LaTeX (compiled to pdf) and (compiled to ps), Coq, Isabelle, and HOL definitions. Most simply, the tool can be used to aid completely informal LaTeX mathematics. Here it permits the definition, and terms within proofs and exposition, to be written in a clear, editable, ASCII notation, without LaTeX noise. It generates good-quality typeset output. By parsing (and so sort-checking) this input, it quickly catches a range of simple errors, e.g. inconsistent use of judgement forms or metavariable naming conventions.

Author: Graham Hutton Abstract: In functional programming, fold is a standard operator that encapsulates a simple pattern of recursion for processing lists. This article is a tutorial on two key aspects of the fold operator for lists. First of all, we emphasize the use of the universal property of fold both as a proof principle that avoids the need for inductive proofs, and as a definition principle that guides the transformation of recursive functions into definitions using fold.

Abstract: Haskell benefits from a sophisticated type system, but implementors, programmers, and researchers suffer because it has no formal description. To remedy this shortcoming, we present a Haskell program that implements a Haskell typechecker, thus providing a mathematically rigorous specification in a notation that is familiar to Haskell users.

Yong Luo mplementation of a Type Theory with Partially Defined Functions and Pattern Matching Foundation: The theoretical foundation of this implementation are based upon my recent talk at Durham on "A Type Theory with Partially Defined Functions". This development challenges the conventional idea that all functions must be defined by means of eliminators and hence all functions must be total. This new theory allows partially defined functions and keeps all the nice properties such as Logical Consistence, Strong Normalisation and Church-Rosser. In this implementation, functions can be defined by pattern-matching. The definition of structural smallness is more powerful, and some termination methods are employed. Programs like "Quick Sort" are allowed in the current implementation.

Research Interests * Semantics of functional programs based on graph rewriting. * Logic, formal verification and computer assisted reasoning. * Dependent type theory with partially defined functions and pattern matching. * Inheritance, reuse and coercive subtyping in type theory. * Functional programming languages with dependent types.

Isabelle is a popular generic theorem proving environment developed at Cambridge University (Larry Paulson) and TU Munich (Tobias Nipkow).

Poly/ML is an implementation of SML. Installation instrucitons of Isabelle suggests Polyml.

Authors: Richard Bird, Ross Paterson Nested datatypes generalise regular datatypes in much the same way that context-free languages generalise regular ones. Although the categorical semantics of nested types turns out to be similar to the regular case, the fold functions are more limited because they can only describe natural transformations. Practical considerations therefore dictate the introduction of a generalised fold function in which this limitation can be overcome. In the paper we show how to construct generalised folds systematically for each nested datatype, and show that they possess a uniqueness property analogous to that of ordinary folds. As a consequence, generalised folds satisfy fusion properties similar to those developed for regular datatypes. Such properties form the core of an effective calculational theory of inductive datatypes.