## User login## Navigation |
## Lambda Calculus## GÃ¶del, Nagel, minds and machines Solomon Feferman. GÃ¶del, Nagel, minds and machines. Ernest Nagel Lecture, Columbia University, Sept. 27, 2007.
This is not directly PLT related, and more philosophical than what we usually discuss on LtU, but I think it will be of interest to some members of the community. While the historical details are interesting, I am not sure I agree with the analysis. It would be interesting to here what others make of this. To make this item slightly more relevant to LtU, let me point out that both the LC and category theory are mentioned (although they are really discussed only in the references). By Ehud Lamm at 2007-10-25 23:46 | General | History | Lambda Calculus | 62 comments | other blogs | 13620 reads
## On One-Pass CPS TransformationsOlivier Danvy, Kevin Millikin and Lasse R. Nielsen. On One-Pass CPS Transformations. March 2007.
Also in JFP 17:793-812 (2007). By Ehud Lamm at 2007-10-23 05:59 | Lambda Calculus | login or register to post comments | other blogs | 7767 reads
## Binary Lambda Calculus and Combinatory LogicWhile Anton was waxing about Church & Turing, I figured that Occam's Razor would be the type of proof one would postulate when giving the nod to Lambda Calculus over Universal Turing Machines. This leads inexorably to the question of what is the smallest (as measured in binary bits) Turing Machine that can possibly be constructed. John Tromp provides an answer to this question in his always fun Lambda Calculus and Combinatory Logic Playground:
Interestingly, the version based on the Lambda Calculus is smaller than the one on Combinators. A statement I found of interest in the paper about PL's:
Not sure if that statement means that PL research is ultimately doomed. :-) By Chris Rathman at 2007-09-18 20:10 | Fun | Lambda Calculus | 23 comments | other blogs | 14240 reads
## Compiling with Continuations, ContinuedCompiling with Continuations, Continued, Andrew Kennedy. ICFP 2007.
By neelk at 2007-08-17 21:15 | Implementation | Lambda Calculus | 7 comments | other blogs | 19429 reads
## Analyzing the Environment Structure ofHigher-Order Languages using Frame StringsAnalyzing the Environment Structure of Higher-Order Languages using Frame Strings, Matthew Might and Olin Shivers. 2007.
Even if you're not interested in flow analysis of functional languages, the preface to this paper is very enjoyable reading. (If you are interested in flow analysis, the whole thing is enjoyable reading. I want a couple of weeks to go through this paper in detail.) By neelk at 2007-08-16 16:23 | Functional | Lambda Calculus | Semantics | 7 comments | other blogs | 7377 reads
## Lambda: The Semantics Tool
We discussed how the LC is used in linguistics in the past (check the archives). This tool may be useful even for those not interested in this angle, even though that's the intended use of the software. ## Lambda AnimatorLambda Animator from Mike Thyer is a tool for displaying and experimenting with alternate reduction strategies in the LC. The tool can use a number of reduction strategies, including completely lazy evaluation. The tool can be invoked in several different modes (via JWS or as an applet), and contains many examples, and the documentation provides clear definitions of the sometime confusing terminology in the field. Notice that the "step" and "run" buttons only work when rendering new graphs, which only works if you are running in trusted mode and have Graphviz installed. Otherwise you'll have to use the the up/down cursor keys or the scroll bar to review already rendered graphs (which exist for all the examples). The site list relevant papers and dissertations. ## LC for kids (alligators, oh my!)(via Wadler) You can show it to the kids, or try to guess what each element in the game represents before reading the explanation at the end... ## Decidability of Higher Order MatchingDecidability of Higher Order Matching, Colin Stirling.
This paper is very technical, but I think it's a problem of significant interest, since decidable fragments of higher-order unification are very important to theorem proving systems. As an aside, Huet conjectured that higher order matching was decidable in 1976, so it's taken thirty years of effort to prove this. ## Light 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 lambda-terms 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.) proof-nets 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 Levy-optimality 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 Curry-Howard-like correspondence between Lamping graphs and proof nets of weakened linear logics. Recommended reading for LtUers who enjoy a challenge! |
## Browse archives## Active forum topics |

## Recent comments

2 hours 30 min ago

2 hours 44 min ago

3 days 15 hours ago

4 days 5 hours ago

4 days 8 hours ago

6 days 6 hours ago

6 days 7 hours ago

6 days 9 hours ago

6 days 16 hours ago

6 days 20 hours ago