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 »