## User login## Navigation |
## Lambda Calculus## Natural Deduction for Intuitionistic Non-Commutative Linear LogicNatural Deduction for Intuitionistic Non-Commutative Linear Logic, Jeff Polakow and Frank Pfenning. TLCA 1999.
My earlier post on linguistics reminded me of the Lambek calculus, which is an ordered logic invented in 1958(!) to model how to parse sentences. So I wanted to find a paper on ordered logic (ie, you can't freely swap the order of hypotheses in a context) and link to that. By neelk at 2007-11-05 17:08 | Lambda Calculus | Type Theory | login or register to post comments | other blogs | 5736 reads
## 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 | 14173 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 | 7863 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 | 14571 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 | 19952 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 | 7509 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. |
## Browse archives## Active forum topics |

## Recent comments

3 days 19 hours ago

4 days 14 hours ago

4 days 18 hours ago

4 days 19 hours ago

4 days 20 hours ago

4 days 20 hours ago

4 days 21 hours ago

4 days 21 hours ago

5 days 1 hour ago

5 days 2 hours ago