Lambda the Ultimate

Cforall is a language design extending ISO C.

Cforall extends the C type-system using overloading, parametric polymorphism, and type generators. … [The] Cforall type system is based on parametric polymorphism, the ability to declare functions with type parameters, rather than an object-oriented type system.

Having been entirely too dismissive of one of Nick Benton's papers before, it seems only fitting that I should attempt expiation for my sins by discussing Formalizing and Verifying Semantic Type Soundness of a Simple Compiler:

We describe a semantic type soundness result, formalized in the Coq proof assistant, for a compiler from a simple imperative language with heap-allocated data into an idealized assembly language. Types in the high-level language are interpreted as binary relations, built using both second-order quantification and a form of separation structure, over stores and code pointers in the low-level machine.

I found this work striking for its strong defense of the utility of semantic, vs. syntactic, type soundness, and for its use of logical relations vs. unary predicates. I could swear that I recently read another paper making quite similar observations about semantic vs. syntactic type soundness. I'm not sure which paper it was, but regardless, there seems to me to be a great deal of overlap of insight and, to a lesser extent, approach, with A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language, and of course by extension to Leroy's work on formalizing big-step operational semantics, allocation, etc. Finally we have the very exciting news about progress on a mechanized metatheory for Standard ML, in Twelf. It's a very exciting time for mechanized metatheory! I'd love to get at least Nick Benton, Adam Chlipala, Xavier Leroy, and Tim Sweeney in a room for a few months so they could create the Next Mainstream Programming Language in Coq. Of course, we have Dr. Benton, Mr. Chlipala, and Mr. Sweeney right here on LtU... :-)

Update: Mea culpa; the paper I had in mind was A Very Modal Model of a Modern, Major, General Type System. It would seem that Dr. Benton, Mr. Chlipala, and Dr. Appel and colleagues have arrived at quite similar perspectives on good approaches to mechanizing metatheory for very interesting programming language design efforts.

Towards a Mechanized Metatheory of Standard ML, Daniel K. Lee, Karl Crary, and Robert Harper.

We present an internal language with equivalent expressive power to Standard ML, and discuss its formalization in LF and the machine-checked verification of its type safety in Twelf. The internal language is intended to serve as the target of elaboration in an elaborative semantics for Standard ML in the style of Harper and Stone. Therefore, it includes all the programming mechanisms necessary to implement Standard ML, including translucent modules, abstraction, polymorphism, higher kinds, references, exceptions, recursive types, and recursive functions. Our successful formalization of the proof involved a careful interplay between the precise formulations of the various mechanisms, and required the invention of new representation and proof techniques of general interest.

The way that most programming languages end up working is by defining a smaller core language to which the constructions in the base language are translated. This means that you can prove the type-safety of a programming language by showing that the internal language is type safe, and that every type-correct program in the full language translates to a type-correct expression in the internal language. In this paper, the authors carried out the mechanization of a core language for SML. The next step is mechanizing the correctness of an elaborator from SML to this core language, and then full, no-foolin' SML will have a fully machine-checked correctness proof.

A Certified Type-Preserving Compiler from Lambda Calculus to Assembly Language

I present a certified compiler from simply-typed lambda calculus to assembly language. The compiler is certified in the sense that it comes with a machine-checked proof of semantics preservation, performed with the Coq proof assistant. The compiler and the terms of its several intermediate languages are given dependent types that guarantee that only well-typed programs are representable. Thus, type preservation for each compiler pass follows without any significant "proofs" of the usual kind. Semantics preservation is proved based on denotational semantics assigned to the intermediate languages. I demonstrate how working with a type-preserving compiler enables type-directed proof search to discharge automatically large parts of the proof obligations.

Software/proof source code and documentation

Slides are available from a talk I gave at the Projet Gallium seminar at INRIA Rocquencourt, in OpenOffice and PDF formats.

I found this while attempting to follow up on this post. The approach taken here—dependently-typed ASTs and denotational semantics—and the observation that, carried to its logical conclusion, the result is typed intermediate and assembly languages, proof-carrying code, etc. suggests to me a connection to this work. It also seems to offer a denotational counterpoint to Leroy's coinductive big-step operational semantics, also done in Coq. Fascinating stuff.

We are pleased to announce the Twelf Wiki, a major new source of documentation about Twelf:

http://twelf.plparty.org

Twelf is a tool used to specify, implement, and prove properties of deductive systems. The Twelf Wiki includes:

• A new introduction to LF and Twelf.
• Tutorials on common Twelf tricks and techniques.
• Case studies of larger applications of Twelf, including encodings of and proofs about linear logic, mutable state, and CPS conversion.
• Pre-compiled CVS builds of Twelf for Linux and Windows.

We invite you to come share what you know, learn from what's there, and ask questions about what's not.

- The Twelf Wiki Team

(I know many of the people working on this, and they've put in a lot of effort to make a really useful resource.)

A Topos Foundation for Theories of Physics: I. Formal Languages for Physics. Andreas Döring and Chris Isham.

This paper is the first in a series whose goal is to develop a fundamentally new way of constructing theories of physics. The motivation comes from a desire to address certain deep issues that arise when contemplating quantum theories of space and time. Our basic contention is that constructing a theory of physics is equivalent to finding a representation in a topos of a certain formal language that is attached to the system. Classical physics arises when the topos is the category of sets. Other types of theory employ a different topos. In this paper we discuss two different types of language that can be attached to a system, S. The first is a propositional language, PL(S); the second is a higher-order, typed language L(S). Both languages provide deductive systems with an intuitionistic logic. The reason for introducing PL(S) is that, as shown in paper II of the series, it is the easiest way of understanding, and expanding on, the earlier work on topos theory and quantum physics. However, the main thrust of our programme utilises the more powerful language L(S) and its representation in an appropriate topos.

This is a little outside of our usual areas, but I think it will appeal to at least some readers. Personally, I find the approach aesthetically very, very appealing for several reasons, and I would be thrilled if an answer to quantum cosmology came from this direction, but I'm the first to admit that my grasp of the phsyics is barely enough to follow along. I was able to make it through this paper fairly easily, but things aren't too interesting in the classical case, and I sadly suspect that the application to quantum physics in parts II and III will leave me behind.

Via The n-Category Cafe, where there is also considerable discussion, much of it around the single word "peristalithic"...

An Intensional Type Theory: Motivation and Cut-Elimination, Paul C. Gilmore.

By the theory TT is meant the higher order predicate logic with the following recursively defined types:

(1) 1 is the type of individuals and [] is the type of the truth values;
(2) [Ï„1, ..., Ï„n] is the type of the predicates with arguments ofthe types Ï„1, ..., Ï„n.

The theory ITT described in this paper is an intensional version of TT. The types of ITT are the same as the types of TT, but the membership of the type 1 of individuals in ITT is an extension of the membership in TT. The extension consists of allowing any higher order term, in which only variables of type 1 have a free occurrence, to be a term of type 1. This feature of ITT is motivated by a nominalist interpretation of higher order predication. In ITT both well-founded and non-well-founded recursive predicates can be defined as abstraction terms from which all the properties of the predicates can be derived without the use of non-logical axioms.

The elementary syntax, semantics, and proof theory for ITT are defined. A semantic consistency proof for ITT is provided and the completeness proof of Takahashi and Prawitz for a version of TT without cut is adapted for ITT; a consequence is the redundancy of cut.

Russell showed Frege's original foundations of mathematics inconsistent when he invented Russell's paradox -- does the set of all sets that do not contain themselves contain itself? This paradox arises because Frege's logic contained an unrestricted comprehension principle -- you could create a set from any predicate. This allows you to cook up vicious cycles such as in Russell's paradox, and the traditional method (invented by Russell) for avoiding these cycles is to allow quantification in a predicative hierarchy: when you comprehend a predicate at level i, you create a set at level i+1, and a predicate at a given level can never mention sets at a higher level.

This paper claims that you can allow unrestricted impredicative quantification if you keep careful track of Frege's sense-reference distinction, and distinguish between predicates and names of predicates. This (if it really works -- I haven't done more than skim the paper yet) would be a different method of using a predicative hierarchy to avoid the paradoxes.

Concoqtion: Indexed Types Now!

Almost twenty years after the pioneering efforts of Cardelli, the programming languages community is vigorously pursuing ways to incorporate F_ω-style indexed types into programming languages. This paper advocates Concoqtion, a practical approach to adding such highly expressive types to full-fledged programming languages. The approach is applied to MetaOCaml using the Coq proof checker to conservatively extend Hindley-Milner type inference. The implementation of MetaOCaml Concoqtion requires minimal modifications to the syntax, the type checker, and the compiler; and yields a language comparable in notation to the leading
proposals. The resulting language provides unlimited expressiveness in the type system while maintaining decidability. Furthermore, programmers can take advantage of a wide range of libraries not only for the programming language but also for the indexed types. Programming in MetaOCaml Concoqtion is illustrated with small examples and a case study implementing a statically-typed domain-specific language.

The follow-up to Concoqtion: Mixing Indexed Types and Hindley-Milner Type Inference, discussed earlier. Good stuff.

Update: There's now a public Concoqtion web site!

Josh, does this answer your question? :-)

Static Typing for a Faulty Lambda Calculus. David Walker. Lester Mackey. Jay Ligatti, George A. Reis, and David I. August.

A transient hardware fault occurs when an energetic particle strikes a transistor, causing it to change state. These faults do not cause permanent damage, but may result in incorrect program execution by altering signal transfers or stored values. While the likelihood that such transient faults will cause any significant damage may seem remote, over the last several years transient faults have caused costly failures in high-end machines at America Online, eBay, and the Los Alamos Neutron Science Center, among others. Because susceptibility to transient faults is proportional to the size and density of transistors, the problem of transient faults will become increasingly important in the coming decades.

This paper defines the first formal, type-theoretic framework for studying reliable computation in the presence of transient faults. More specifically, it defines lambda-zap, a lambda calculus that exhibits intermittent data faults. In order to detect and recover from these faults, lambda-zap programs replicate intermediate computations and use majority voting, thereby modeling software-based fault tolerance techniques studied extensively, but informally.

To ensure that programs maintain the proper invariants and use lambda-zap primitives correctly, the paper defines a type system for the language. This type system guarantees that well-typed programs can tolerate any single data fault. To demonstrate that lambda-zap can serve as an idealized typed intermediate language, we define a type-preserving translation from a standard simply-typed lambda calculus into lambda-zap.

Lightweight static resources: Sexy types for embedded and systems programming. Oleg Kiselyov and Chung-chieh Shan.

It is an established trend to develop low-level code—embedded software, device drivers, and operating systems—using high-level languages, especially the advanced abstraction facilities in functional programming. To be reliable and secure, low-level
code must correctly manage space, time, and other resources, so special type systems and verification tools arose to regulate resource access statically. However, a general-purpose functional programming language practical today can provide the same static assurances, also with no run-time overhead. We substantiate this claim and promote the trend with two security kernels in the domain of device drivers:
1. one built around raw pointers, to track and arbitrate the size, alignment, write permission, and other properties of memory areas across indexing and casting;
2. the other built around a device register, to enforce protocol and timing requirements while reading from the register.
Our style is convenient in Haskell thanks to custom kinds and predicates (as type classes); type-level numbers, functions, and records (using functional dependencies); and mixed type- and term-level programming (enabling partial type signatures).

The related source code is also available.

Ken and Oleg's work is always worth checking out, so I urge LtU readers to go and see the solutions they propose aimed at allowing programmers of low level system software to work with raw pointers, device registers etc., while statically enforcing invariants such as pointer validity and in-bounds memory access.

The link is to a near final draft of a paper to be presented at TFP2007, and comments - I'm told - will be appreciated, especially as regards the "Related Work" section. Be quick with your comments, though, since the "camera ready" date is tomorrow...