Lambda the Ultimate

March 24th 2007, 6PM

Formal meeting- Intro to Haskell, plus some PARSEC wizardry. Adam Turoff, our resident Haskell guru, will be giving a presentation on said language. If you live near DC and have an interest in Haskell, this'll be your rare opportunity to get exposed to the laziest of functional languages! Plus, we'll have a small presentation on some fun plt-scheme code as an opening act (and, of course, we'll go out for beer as a closing act)

http://www.lisperati.com/fringedc.html

Remarkable little language. This thread on embedded languages got me looking, and I came across this paper:

Embedded microcontrollers are becoming increasingly prolific, serving as the primary or auxiliary processor in products and research systems from microwaves to sensor networks. Microcontrollers represent perhaps the most severely resource-constrained embedded processors, often with as little as a few bytes of memory and a few kilobytes of code space. Language and compiler technology has so far been unable to bring the benefits of modern object-oriented languages to such processors. In this paper, I will present the design and implementation of Virgil, a lightweight object-oriented language designed with careful consideration for resource-limited domains. Virgil explicitly separates initialization time from runtime, allowing an application to build complex data structures during compilation and then run directly on the bare hardware without a virtual machine or any language runtime. This separation allows the entire program heap to be available at compile time and enables three new data-sensitive optimizations: reachable members analysis, reference compression, and ROM-ization. Experimental results demonstrate that Virgil is well suited for writing microcontroller programs, with five demonstrative applications fitting in less than 256 bytes of RAM with fewer than 50 bytes of metadata. Further results show that the optimizations presented in this paper reduced code size between 20% and 80% and RAM size by as much as 75%.

Looks very promising. It's notion of "initialization-time" is worthy of further thought. See also the Virgil homepage, where you can download preliminary source releases. The features page list a number of interesting tidbits as well: Virgil will soon support tail call optimization! In particular, see what's coming in Virgil II:

* Parametric types
* Module system
* Tuples
* Generalized Algebraic Types
* Integration with non-Virgil code

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.