User loginNavigation 
Lambda CalculusA 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  6253 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  5318 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  27480 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  31290 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  5195 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  4680 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  6280 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  10099 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  23528 reads
Ivor, a proof engineI found an interesting new paper by Edwin Brady.
By Niels Hoogeveen at 20060808 13:39  Functional  Lambda Calculus  Type Theory  1 comment  other blogs  5492 reads

Browse archivesActive forum topics 
Recent comments
3 hours 29 min ago
6 hours 48 min ago
2 days 1 hour ago
2 days 2 hours ago
2 days 8 hours ago
2 days 10 hours ago
2 days 18 hours ago
2 days 18 hours ago
2 days 19 hours ago
2 days 21 hours ago