User loginNavigation 
Lambda CalculusIvor, 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  5655 reads
Jumbo 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  12673 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  6950 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  7724 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  10654 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  8164 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  5211 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  4178 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  7132 reads

Browse archivesActive forum topics 
Recent comments
2 days 3 hours ago
2 days 22 hours ago
3 days 2 hours ago
3 days 3 hours ago
3 days 4 hours ago
3 days 4 hours ago
3 days 5 hours ago
3 days 5 hours ago
3 days 9 hours ago
3 days 9 hours ago