User loginNavigation 
Lambda CalculusThe Experimental Effectiveness of Mathematical ProofThe Experimental Effectiveness of Mathematical Proof
I thought I had already posted this, but apparently not. Consider this paper the main gauntlet thrown down to those who insist that mathematical logic, the CurryHoward Isomorphism, etc. might be fine for "algorithmic code" (as if there were any other kind) but is somehow inapplicable the moment a system interacts with the "real" or "outside" world (as if software weren't real). Update: the author is Alexandre Miquel, and the citation is "Chapitre du livre Anachronismes logiques, Ã paraÃ®tre dans la collection Logique, Langage, Sciences, Philosophie, aux Publications de la Sorbonne. Ã‰d.: Myriam Quatrini et Samuel TronÃ§on, 2010." By Paul Snively at 20111030 16:05  Functional  Lambda Calculus  Logic/Declarative  Semantics  32 comments  other blogs  13740 reads
Levy: 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  31830 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  11181 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  13577 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  7549 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  8229 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  9275 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  9048 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  10401 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  13505 reads

Browse archivesActive forum topics 
Recent comments
2 hours 5 min ago
4 hours 5 min ago
9 hours 59 min ago
1 day 2 hours ago
1 day 11 hours ago
1 day 22 hours ago
1 day 23 hours ago
2 days 1 min ago
2 days 1 hour ago
2 days 1 hour ago