User loginNavigation 
Lambda CalculusLight Logics and Optimal Reduction
Not sure this isn't a tad too technical for the front page, but posting has been light, so...
Baillot, Coppola & Del Lago have an arXived preprint, "Light Logics and Optimal Reduction: Completeness and Complexity: Typing of lambdaterms in Elementary and Light Affine Logic (EAL, LAL, resp.) has been studied for two different reasons: on the one hand the evaluation of typed terms using LAL (EAL, resp.) proofnets admits a guaranteed polynomial (elementary, resp.) bound; on the other hand these terms can also be evaluated by optimal reduction using the abstract version of Lamping's algorithm. The first reduction is global while the second one is local and asynchronous. We prove that for LAL (EAL, resp.) typed terms, Lamping's abstract algorithm also admits a polynomial (elementary, resp.) bound. We also show its soundness and completeness (for EAL and LAL with type fixpoints), by using a simple geometry of interaction model (context semantics). We've 'known' that Lamping's algorithm implements Levyoptimality since Lamping 'proved' it in 1989, but unfortunately his argument has holes, and it has proven hard to fix them, this despite there being a fairly accessible geometric intuition supporting soundness & completeness. Harry Mairson has done worthy missionary work advertising the importance of this gap and working towards filling it. I haven't yet worked my way through this proof, but it looks like it belongs to a very attractive class of argument; namely those that attempt to forge a CurryHowardlike correspondence between Lamping graphs and proof nets of weakened linear logics. Recommended reading for LtUers who enjoy a challenge! A Logic for Parametric PolymorphismA Logic for Parametric Polymorphism, Gordon Plotkin and MartÃn Abadi.
By neelk at 20070413 22:27  Category Theory  Lambda Calculus  Semantics  Theory  login or register to post comments  other blogs  6410 reads
RZ: a tool for bringing constructive and computable mathematics closer to programming practiceRZ: a tool for bringing constructive and computable mathematics closer to programming practice, Chris Stone and Andrej Bauer.
Realizability is a way of formalizing the constructive interpretation of logical formulas (eg, the BHK interpretation). Constructively, a proof of an implication By neelk at 20070410 22:57  DSL  Lambda Calculus  Semantics  3 comments  other blogs  5488 reads
Verifying Semantic Type Soundness of a Simple CompilerHaving 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:
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 TypePreserving Compiler from Lambda Calculus to Assembly Language, and of course by extension to Leroy's work on formalizing bigstep 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. By Paul Snively at 20070404 04:45  Implementation  Lambda Calculus  Type Theory  login or register to post comments  other blogs  28005 reads
A Certified TypePreserving Compiler from Lambda Calculus to Assembly LanguageA Certified TypePreserving Compiler from Lambda Calculus to Assembly Language
I found this while attempting to follow up on this post. The approach taken here—dependentlytyped ASTs and denotational semantics—and the observation that, carried to its logical conclusion, the result is typed intermediate and assembly languages, proofcarrying code, etc. suggests to me a connection to this work. It also seems to offer a denotational counterpoint to Leroy's coinductive bigstep operational semantics, also done in Coq. Fascinating stuff. By Paul Snively at 20070322 15:46  Functional  Implementation  Lambda Calculus  MetaProgramming  Semantics  Type Theory  14 comments  other blogs  32232 reads
Lightweight Fusion by Fixed Point PromotionLightweight Fusion by Fixed Point Promotion, Atsushi Ohori and Isao Sasano.
Deforestation is one of those optimizations every functional programmer who has ever had to rewrite a beautiful composition of maps and filters into an evil, ugly explicit fold has always longed for. Unfortunately, the standard lightweight fusion algorithms have trouble with examples as simple as By neelk at 20070212 23:52  Functional  Implementation  Lambda Calculus  4 comments  other blogs  5461 reads
The Theory of Parametricity in Lambda Cube
Parametricity is Wadler gets his theorems for free, nad Izumi gives an example of one of these free theorems for dependent sums in the Calculus of Constructions. By Jim Apple at 20061127 13:52  Lambda Calculus  Semantics  Type Theory  login or register to post comments  other blogs  4802 reads
Holodeck games and CCCsFrom the nCategory Cafe, some notes on Holodeck Games and cartesian closed categories. This also appeared here (and was mentioned by Phil Wadler). The two posts seem to have different addenda, comments and links, so it may be worth looking at both. It's fun to see lambda calculus introduced to an audience already familiar with categories, as that seems to be the opposite of the usual state of affairs around here, and I can think of certain LtU regulars who will hopefully find this whole subject enjoyable. By Matt Hellige at 20061023 23:03  Category Theory  Fun  Lambda Calculus  login or register to post comments  other blogs  6427 reads
Arrows, like Monads, are MonoidsBy Chris Heunen and Bart Jacobs
By Jim Apple at 20060930 19:04  Category Theory  Functional  Lambda Calculus  3 comments  other blogs  10395 reads
Gradual Typing for Functional LanguagesGradual Typing for Functional Languages
In other news, the Holy Grail has been found. Film at 11. This piece of genius is the combined work of Jeremy Siek, of Boost fame, and Walid Taha, of MetaOCaml fame. The formalization of their work in Isabelle/Isar can be found here. I found this while tracking down the relocated Concoqtion paper. In that process, I also found Jeremy Siek's other new papers, including his "Semantic Analysis of C++ Templates" and "Concepts: Linguistic Support for Generic Programming in C++." Just visit Siek's home page and read all of his new papers, each of which is worth a story here. By Paul Snively at 20060830 17:49  Functional  Implementation  Lambda Calculus  Semantics  Type Theory  18 comments  other blogs  25560 reads

Browse archivesActive forum topics 
Recent comments
1 week 2 days ago
1 week 2 days ago
1 week 3 days ago
1 week 3 days ago
1 week 3 days ago
1 week 3 days ago
1 week 3 days ago
1 week 3 days ago
1 week 3 days ago
1 week 3 days ago