Lambda the Ultimate

Why Dependent Types Matter. Thorsten Altenkirch Conor McBride James McKinna

We exhibit the rationale behind the design of Epigram, a dependently typed programming language and interactive program development system using refinements of a well known program, merge sort, as a running example. We discuss the relationship to other proposals to introduce aspects of dependent types into functional programming languages and sketch some topics for further work in this area.

Epigram, dependent types, general reucrsion, indexed datatypes - it's all here!

Enjoy.

The summer school, Proofs of Programs and Formalisation of Mathematics, is in Goteborg, Sweden, August 15-26.

You might still apply for a grant, but time is short!

Only a tentative program is currently available, but I suppose the topics mentioned in it will remain in the final program, and many of them are interesting, and often discussed here on LtU.

Some of you might be interested in subtext, a project that explores the idea of example centric programming and non-textual programs.

The basic idea is that the representation of a program is the same as its execution (possibly related to the discussion currently going on about edit-time, reasoning-time etc.)

Programs are constructed by copying and executed copy flow: the projection of changes through copies.

If all this sounds intriguing, hop over and take a look. The site hosts a couple of demos and papers that provide more details.

Spec# is an extension of C#. It extends the type system to include non-null types and checked exceptions. It provides method contracts in the form of pre- and postconditions as well as object invariants.

The Spec# static program verifier. This component translates Spec# programs into logical verification conditions. Internally it uses an automatic theorem prover that operates on the verification conditions deduced from the Spec# contract. An interface to the Spec Explorer tool for test generation and model-based testing.

A unique feature of the Spec# programming system is its guarantee of maintaining invariants in object-oriented programs in the presence of callbacks, threads and inter-object relationships.

Spec# (also "specsharp" for search engines and the like), is now available for download. The home page gives a list of related publications.

by Jim Gray, via Joe Armstrong and apropos Crash-only software.

An analysis of the failure statistics of a commercially available fault-tolerant system shows that administration and software are the major contributors to failure. Various approaches to software fault-tolerance are then discussed -- notably process-pairs, transactions and reliable storage. It is pointed out that faults in production software are often soft (transient) and that a transaction mechanism combined with persistent process-pairs provides fault-tolerant execution -- the key to software fault-tolerance.

Link

For those who do not think that "catamorphism" sounds scary, Generic Accumulations paper presents a new flavor of fold: fold with accumulators (afold).

You might be acquainted with its cousin - pfold, or fold with parameters. Both come from the family of comonadic fold.

A homepage of Alberto Pardo contains more information on them.

PS: if you are new to fold or bananas/lenses, LtU papers page has a couple of introductory links.

ACM Symposium on Dynamic Languages
October 18, 2005, San Diego, California
(co-located with OOPSLA'05)
URL: http://decomp.ulb.ac.be:8082/events/dls05/

Currently, the dynamic language community is fragmented, split over a multitude of paradigms (from functional over logic to object-oriented), languages and syntaxes. This fragmentation severely hinders research as well as acceptance, and results in either language wars or, even worse, language ignorance. The goal of this symposium is to provide a highly visible, international forum for researchers working on dynamic features and languages. We explicitly invite submissions from all kinds of paradigms (object-oriented, functional, logic, ...), as can be seen from the structure of the program committee.

DLS'05 invites the submission of technical papers presenting research results or experience in all areas related to dynamic languages or dynamic language concepts. Research papers should describe work that advances the current state of the art. Experience reports should be of broad interest and should describe insights gained from the practical application of dynamic languages that are of use to other researchers and practitioners. The program committee will evaluate each contributed research and experience paper based on its relevance, significance, clarity, originality, and correctness.

Areas of interests include, but are not limited to:
-closures
-delegation
-actors, active objects
-constraint systems
-mixins and traits
-reflection and meta-programming
-aspect-oriented programming in dynamic environments
-language symbiosis and multi-paradigm languages
-experience reports on successful application of dynamic languages

Papers will be published in the ACM Digital Library.

More information (submission guidelines, dates, program committee) can be found on http://decomp.ulb.ac.be:8082/events/dls05/

PMAT analyzes IBM verbose GC traces by parsing the traces and building pattern models. PMAT recommends key configurations by executing a diagnosis engine and pattern modeling algorithm. If there are any errors related with Java heap exhaustion or fragmentation in the verbose GC trace, PMAT can diagnose the root cause of failures. PMAT provides rich chart features that graphically display Java heap usage.

Sounds useful. If anyone has the time to download and check this out, it would be interesting to hear what you think.

Lambdascope:
Another optimal implementation of the lambda-calculus

We have presented an implementation of the lambda-calculus
in the spirit of the calculational approach [...], and which
is fully in the traditions of calculi with explicit substitution
and of graph implementations of term rewriting. As far as
we know it is the first such calculus which is optimal in the sense of Levy. Moreover, as far as we know this is the
first optimal calculus featuring only a single scope delimiter
node instead of the usual two, croissants and brackets,
which by force eliminates the problems which are caused by
having more than one scope node [...]. The calculus
is simple, half a page suffices [...] to describe
it, and completely reduction-based (no semantic read-back
in the implementation). As a consequence it can be trivially
implemented in any (modern) programming language.

Remembering our discussion on atoms of PLs (such as scope and name), I decided this paper might be of interest.

If you haven't seen the AOP blog you might want to check it out.

Via the blog we find the AOSD discssion titled AOP considered harmful which, not surprisingly, is quite heated :-).

It has been awhile since we discussed AOP, but I know many LtU regulars are skeptical about AOP, as am I. It's interesting to look at the discussion from the other sides point of view.