User loginNavigation 
Lambda CalculusLevy: a Toy CallbyPushValue LanguageAndrej Bauer's blog contains the PL Zoo project. In particular, the Levy language, a toy implementation of Paul Levy's CBPV in OCaml. If you're curious about CBPV, this implementation might be a nice accompaniment to the book, or simply a hands on way to check it out. It looks like an implementation of CBPV without sum and product types, with complex values, and without effects. I guess a more handson way to get to grips with CBPV would be to implement any of these missing features. The posts are are 3 years old, but I've only just noticed them. The PL Zoo project was briefly mentioned here. By Ohad Kammar at 20110714 18:57  Fun  Functional  Implementation  Lambda Calculus  Paradigms  Semantics  Teaching & Learning  Theory  4 comments  other blogs  31348 reads
Milawa: A SelfVerifying Theorem Prover for an ACL2Like LogicMilawa: A SelfVerifying Theorem Prover for an ACL2Like Logic
This might help inform discussions of the relationship between the de Bruijn criterion (the "social process" of mathematics) and formal verification. I think it also serves as an interesting signpost on the road forward: it's one thing to say that starting with a de Bruijn core and evolving a more powerful prover is possible in principle; it's another thing for it to actually have been done. The author's thesis defense slides provide a nice, quick overview. By Paul Snively at 20100529 17:49  DSL  Functional  Implementation  Lambda Calculus  Logic/Declarative  Semantics  11 comments  other blogs  10674 reads
A Lambda Calculus for Real AnalysisA Lambda Calculus for Real Analysis
Paul Taylor is deadly serious about the intersection of logic, mathematics, and computation. I came across this after beating my head against Probability Theory: The Logic of Science and Axiomatic Theory of Economics over the weekend, realizing that my math just wasn't up to the tasks, and doing a Google search for "constructive real analysis." "Real analysis" because it was obvious that that was what both of the aforementioned texts were relying on; "constructive" because I'd really like to develop proofs in Coq/extract working code from them. This paper was on the second page of results. Paul's name was familiar (and not just because I share it with him); he translated JeanYves Girard's regrettably outofprint Proofs and Types to English and maintains a very popular set of tools for typesetting commutative diagrams using LaTeX. By Paul Snively at 20100216 22:00  Category Theory  Functional  Lambda Calculus  Logic/Declarative  MetaProgramming  Semantics  Type Theory  9 comments  other blogs  13070 reads
Syntactic Proofs of Compositional Compiler CorrectnessSyntactic Proofs of Compositional Compiler Correctness
A submitted draft of another paper from Adam, continuing to expand LambdaTamer's reach. By Paul Snively at 20100109 17:10  Functional  Implementation  Lambda Calculus  Semantics  Type Theory  4 comments  other blogs  7286 reads
A Verified Compiler for an Impure Functional LanguageA Verified Compiler for an Impure Functional Language
Further work on/with LambdaTamer for certified compiler development. By Paul Snively at 20100109 17:03  Functional  Implementation  Lambda Calculus  Semantics  Type Theory  4 comments  other blogs  7719 reads
Certified Programming With Dependent Types Goes BetaCertified Programming With Dependent Types From the introduction:
This is the best Coq tutorial that I know of, partially for being comprehensive, and partially for taking a very different tack than most with Adam's emphasis on proof automation using Coq's Ltac tactic language. It provides an invaluable education toward understanding what's going on either in LambdaTamer or Ynot, both of which are important projects in their own rights. Please note that Adam is explicitly requesting feedback on this work. By Paul Snively at 20100109 16:56  Functional  Lambda Calculus  Logic/Declarative  Misc Books  Semantics  Teaching & Learning  Type Theory  6 comments  other blogs  8825 reads
A Veriï¬ed Compiler for an Impure Functional LanguageA Veriï¬ed Compiler for an Impure Functional Language
The latest from Adam Chlipala. Yet another evolutionary step for Lambda Tamer. Between this and Ynot the Coq/certified compiler story seems to be getting more impressive nearly daily. By Paul Snively at 20090810 16:09  Functional  Implementation  Lambda Calculus  Semantics  8 comments  other blogs  8730 reads
Oh no! Animated Alligators!Lambda calculus as animated alligators and eggs. Virtually guaranteed to turn any 4 year old into a PLT geek. The nonanimated game was mentioned previously on LTU here. By James Iry at 20090709 18:43  Fun  Functional  Lambda Calculus  Teaching & Learning  8 comments  other blogs  9652 reads
DanaLuke Palmer and Nick Szabo can shoot me for this if they want, but I think this is warranted, and I want to connect a couple of dots as well. Luke is one of a number of computer scientists, with Conal Elliott probably being the best known, who have devoted quite a bit of attention to Functional Reactive Programming, or FRP. FRP has been discussed on LtU off and on over the years, but, unusually for LtU IMHO, does not seem to have gotten the traction that some other similarly abstruse subjects have. In parallel, LtU has had a couple of interesting threads about Second Life's economy, smart contracts, usage control, denial of service, technical vs. legal remedies, and the like. I would particularly like to call attention to this post by Nick Szabo, in which he discusses a contract language that he designed:
In recent private correspondence, Nick commented that he'd determined that he was reinventing synchronous programming Ã la Esterel, and mentioned "Reactive" programming. Ding! To make a potentially long entry somewhat shorter, Luke is working on a new language, Dana, which appears to have grown out of some frustration with existing FRP systems, including Conal Elliot's Reactive, currently perhaps the lynchpin of FRP research. Luke's motivating kickoff post for the Dana project can be found here, and there are several followup posts, including links to experimental source code repositories. Of particularly motivating interest, IMHO, is this post, where Luke discusses FRP's interaction with garbage collection succinctly but nevertheless in some depth. Luke's most recent post makes the connection from Dana, which Luke has determined needs to have a dependentlytyped core, to Illative Combinatory Logic, explicit, and offers a ~100 line type checker for the core. I find this very exciting, as I believe strongly in the project of being able to express computation centered on time, in the sense of Nick's contract language, in easy and safe ways extremely compelling. I've intuited for some time now that FRP represents a real breakthrough in moving us past the Von Neumann runtime paradigm in fundamental ways, and between Conal Elliott's and Luke's work (and no doubt that of others), it seems to me that my sense of this may be borne out, with Nick's contract language, or something like it, as an initial application realm. So I wanted to call attention to Luke's work, and by extension recapitulate Conal's and Nick's, both for the PLT aspects that Luke's clearly represents, but also as a challenge to the community to assist in the realization of Nick's design efforts, if at all possible. By Paul Snively at 20090218 21:55  Functional  General  Implementation  Lambda Calculus  Semantics  Theory  Type Theory  17 comments  other blogs  12870 reads
Parameterized Notions of ComputationParameterized Notions of Computation, Robert Atkey, JFP 2008.
Once you've programmed with monads for a while, it's pretty common to start defining parameterized families of monads  e.g., we might define a family of type constructors for IO, in which the program type additionally tracks which files the computation reads and writes from. This is a very convenient programming pattern, but the theory of it is honestly a little sketchy: on what basis do we conclude that the indices we define actually track what we intend them to? And furthermore, why can we believe that (say) the monadic equational laws still apply? That's the question Atkey lays out a nice solution to. He gives a nice categorical semantics for indexed, effectful computations, and then cooks up lambda calculi whose equational theory corresponds to the equations his semantics justifies. The application to delimited continuations is quite nice, and the type theories can also give a little insight into the basics of how stuff like Hoare Type Theory works (which uses parameterized monads, with a very sophisticated language of parameters). On a slightly tangential note, this also raises in my mind a methodological point. Over the last n years, we've seen many people identify certain type constructors, whose usage is pervasive, and greatly simplified with some syntactic extensions  monads, comonads, applicative functors, arrows, and so on. It's incredible to suggest that we have exhausted the list of interesting types, and so together they constitute a good argument for some kind of language extension mechanism, such as macros. However, all these examples also raise the bar for when a macro is a good idea, because what makes them compelling is precisely that the right syntax yields an interesting and pretty equational theory in the extended language. By neelk at 20090211 21:40  Category Theory  Lambda Calculus  Semantics  Type Theory  16 comments  other blogs  12267 reads

Browse archivesActive forum topics 
Recent comments
7 hours 23 min ago
1 week 1 day ago
1 week 3 days ago
1 week 3 days ago
1 week 3 days ago
1 week 3 days ago
1 week 3 days ago
1 week 3 days ago
1 week 3 days ago
1 week 3 days ago