User loginNavigation 
Lambda CalculusJumbo Lambda CalculusTwo new papers by Paul Blain Levy, "Jumbo Lambda Calculus" and the extended version "Jumbo Connectives in Type Theory and Logic", are available on his web page. Part of the abstract:
(From the types list.) By Matt Hellige at 20060512 16:23  Lambda Calculus  Semantics  Type Theory  3 comments  other blogs  11796 reads
Lambda Calculus course (Oxford)A sixteenhour lecture course aimed at finalyear computer science undergraduates and MSc students. The course notes are detailed and include things like callbyvalue LC, Boehm Theorem, and several interesting miniprojects for students. By Ehud Lamm at 20060319 13:13  Lambda Calculus  login or register to post comments  other blogs  6836 reads
Inverse typechecker and theorem proving in intuitionistic and classical logicsAnother cool demonstration from Oleg:
By Ehud Lamm at 20060205 09:09  Fun  Lambda Calculus  Type Theory  4 comments  other blogs  7589 reads
Systematic search for lambda expressionsSystematic search for lambda expressions by Susumu Katayama
Although the algorithm is slow and only works on small expressions, it looks helpful. Perhaps there could be some synthesis with Hoogλe, or whatever the name is after Google makes them change it. By Jim Apple at 20051126 15:01  Functional  Lambda Calculus  5 comments  other blogs  10498 reads
What good is Strong Normalization in Programming Languages?There's a neat thread about strong normalization happening on The Types Forum.
Termination is good:
Termination is good!
Termination is good and with fixpoints is turing complete?
Terminating reductions allows exhaustive applications of optimizations:
Rene Vestergaard also gave a link to a 2004 discussion of strong normalization on the rewriting list. By shapr at 20051117 12:31  Implementation  Lambda Calculus  Theory  Type Theory  15 comments  other blogs  7935 reads
adbmaL
... or how is the title of this paper pronounced?
We make the notion of scope in the lambdacalculus explicit. To that end, the syntax of the lambdacalculus is extended with an endofscope operator [adbmal], matching the usual opening of a scope due to lambda. Accordingly, betareduction is extended to the set of scoped lambdaterms by performing minimal scope extrusion before performing replication as usual. We show confluence of the resulting scoped betareduction. Confluence of betareduction for the ordinary lambdacalculus is obtained as a corollary, by extruding scopes maximally before forgetting them altogether. Only in this final forgetful step, alphaequivalence is needed. All our proofs have been verified in Coq.While playing with my own lambdamachine (derivative of CEK in Java) I decided that I would like to control scope better  so I found this paper. See also Lambdascope previously mentioned on LtU. A Concurrent Lambda Calculus with FuturesA Concurrent Lambda Calculus with Futures
To all the fans of Mozart and especially Stockhausen :) By Andris Birkmanis at 20050717 14:05  Functional  Lambda Calculus  login or register to post comments  other blogs  5136 reads
A FormulaeasTypes Interpretation of Subtractive LogicA FormulaeasTypes Interpretation of Subtractive Logic
Yet another connection between subtractive logic and control. I remember the author mentioned on LtU, but I cannot find any citations. By Andris Birkmanis at 20050629 11:46  Functional  Lambda Calculus  Type Theory  1 comment  other blogs  4105 reads
BottomUp betaSubstitution: Uplinks and lambdaDAGsWhile classically lambdaexpressions are seen as trees, people don't stop trying to use more general graphs for their representation (according to the authors, the ideas go back to Bourbaki in 1954).
So it's efficient in both time and space, interactive, and simple to implement! What else is left to desire? By Andris Birkmanis at 20050609 21:16  Functional  Lambda Calculus  3 comments  other blogs  7004 reads
On Evaluation Contexts, Continuations, and the Rest of Computation
Although already mentioned before, I believe this paper (which reconciles two approaches to defining continuations) deserves a separate story.
On Evaluation Contexts, Continuations, and the Rest of Computation Continuations are variously understood as representations of the current evaluation context and as representations of the rest of the computation, but these understandings contradict each other: plugging an expression in a context yields a new expression whereas sending an intermediate result to a continuation yields the final answer. We show that continuationsasevaluationcontexts are the defunctionalized representation of the continuation of a singlestep reduction function and that continuationsastherestofthecomputation are the continuation of an evaluation function. Furthermore, we show that defunctionalizing the continuation of an evaluator gives rise to the same evaluation contexts as in the singlestep reducer. The only difference is how these evaluation contexts are interpreted: a â€˜plugâ€™ interpretation yields onestep reduction, whereas a â€˜refocusâ€™ interpretation yields evaluation. By Andris Birkmanis at 20050608 13:45  Lambda Calculus  Semantics  1 comment  other blogs  4986 reads

Browse archivesActive forum topics 
Recent comments
4 hours 47 min ago
19 hours 19 min ago
21 hours 45 min ago
2 days 20 hours ago
2 days 21 hours ago
2 days 22 hours ago
3 days 6 hours ago
3 days 9 hours ago
3 days 13 hours ago
3 days 13 hours ago