LFMTP 2013 and logical frameworks

8th International Workshop on Logical Frameworks and Meta-Langauges: Theory and Practice (LFMTP 2013)

Robert Harper, Furio Honsell, and Gordon Plotkin. 1993. A framework for defining logics. J. ACM 40, 1 (January 1993), 143-184.

I'm gratuitously attending ICFP 2013 (i.e., I'm not presenting or helping organize, though I was on the LFMTP PC).

This year's LFMTP celebrated the 20th anniversary of the publication of Harper, Honsell and Plotkin's "A framework for defining logics".  I want to say a few words about that work and draw a line connecting it to currently exciting activities in the functional PL world, many of which were presented yesterday at ICFP.

Harper, Honsell and Plotkin introduced LF, which is a dependent type theory (essentially the same as what is often also called $\lambda$P, one of the corners of the lambda cube).  Expressions are classified into kinds, types, and objects; kinds classify types; types classify objects.  Types can depend on objects and kinds on types.

Read more »

Expressive power of programming languages

On the expressive power of programming languages
Matthias Felleisen
Science of Computer Programming 17:1-3(35-75), Dec. 1991

On absraction and the expressive power of programming langauges
John C. Mitchell
Science of Computer Programming 21:2(141-163), Oct. 1993

It is a typical observation in an introductory programming language class that language constructs such as "let" are dispensable in a language with first-class lambda-abstraction, or that different forms of loops, such as while, for, or do-while in C/C++/Java, are interdefinable.  However, the formal content of these observations is not always made clear.

These two papers appeared in the early 90s and seem to describe independently-developed notions of expressiveness and "meaning-preserving translation" among programming languages.  Both notions seek to draw finer distinctions than Turing-completeness - that is, we want to identify a sense in which one Turing-complete language is "more expressive" than another, even though both languages can express the same computable functions over natural numbers (and by Gödel numbering, each can define an evaluator for the other).

Read more »

DBPL 2013

DBPL 2013

I attended DBPL 2013 in Riva Del Garda, Italy - a very attractive venue.  I was stupid and only came for the day of the workshop.  There were a lot of interesting talks.
Read more »