User loginNavigation 
Lambda CalculusPure Subtype SystemsPure Subtype Systems, by DeLesley S. Hutchins:
A thoughtprovoking take on type theory using subtyping as the foundation for all relations. He collapses the type hierarchy and unifies types and terms via the subtyping relation. This also has the sideeffect of combining type checking and partial evaluation. Functions can accept "types" and can also return "types". Of course, it's not all sunshine and roses. As the abstract explains, the metatheory is quite complicated and soundness is still an open question. Not too surprising considering type checking Type:Type is undecidable. Hutchins' thesis is also available for a more thorough treatment. This work is all in pursuit of Hitchens' goal of featureoriented programming. By naasking at 20131108 23:53  Lambda Calculus  ObjectFunctional  OOP  Type Theory  39 comments  other blogs  11774 reads
DependentlyTyped Metaprogramming (in Agda)Conor McBride gave an 8lecture summer course on Dependently typed metaprogramming (in Agda) at the Cambridge University Computer Laboratory:
The lecture notes, code, and video captures are available online. As with his previous course, the notes contain many(!) mind expanding exploratory exercises, some of which quite challenging. By Ohad Kammar at 20130830 07:34  Category Theory  Functional  Lambda Calculus  MetaProgramming  Paradigms  Semantics  Teaching & Learning  Theory  Type Theory  5 comments  other blogs  10625 reads
Mechanized λ<sub>JS</sub>Mechanized λ_{JS}
More work on mechanizing the actual, implemented semantics of a real language, rather than a toy. By Paul Snively at 20120627 15:28  Functional  Javascript  Lambda Calculus  Semantics  6 comments  other blogs  10485 reads
Milawa on Jitawa: a Verified Theorem Prover
This is pretty interesting: Milawa was already "selfverifying," in the sense explained on the page. More recently, it's been made to run on a verified Lisp runtime, so that means the entire stack down to the X86_64 machine code is verified. Milawa itself is "ACL2like," so it's not as interesting logically as, say, Isabelle or Coq, but it's far from a toy. Also, the Jitawa formalization apparently took place in HOL4, so you need to trust HOL4. Since HOL4 is an "LCFlike" system, you can do that to the extent that you trust the LCF process, but it doesn't satisfy the de Bruijn criterion in the same way Milawa or Coq do. Nevertheless, this seems like an important step toward the ultimate goal of having a stack that is verified "all the way down," as it were. By Paul Snively at 20120229 18:34  Functional  Lambda Calculus  Logic/Declarative  2 comments  other blogs  6441 reads
Vellvm: Formalizing the LLVM Intermediate Representation for Verified Program TransformationsVellvm: Formalizing the LLVM Intermediate Representation for Verified Program Transformations by Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic, POPL 2012
This obviously represents huge progress in marrying the theoretical benefits of tools like Coq with the practical benefits of tools like LLVM. We can only hope that this spurs further development in practical certified software development. By Paul Snively at 20120128 15:57  Functional  Lambda Calculus  Semantics  Type Theory  16 comments  other blogs  10442 reads
Deca, an LtUfriendly bare metal systems programming languageThe Deca programming language is "a language designed to provide the advanced features of sophisticated, highlevel programming languages while still programming as close as possible to the bare metal. It brings in the functional, objectoriented, and generic programming paradigms without requiring a garbage collector or a threading system, so programmers really only pay in performance for the features they use." The latter link provides a list of features that Deca does, will, and won't provide. Features provided include type inference, universally and existentially quantified types, and "a strong regionandeffect system that prohibits unsafe escaping pointers and doublefree errors". The Deca language and ideas behind it are documented in a thesis, The design and implementation of a modern systems programming language (PDF):
The source code for the Deca compiler, decac, is available here. The compiler is implemented in Scala and generates LLVM bytecode. (The author points out in the comments below that this implementation is a work in progress.) The author of Deca is LtU member Eli Gottlieb, who back in 2008 posted in the forum asking for feedback on his language: Practical Bits of Making a Compiler for a New Language. There's some more discussion of Deca over at Hacker News. By Anton van Straaten at 20120102 02:40  Implementation  Lambda Calculus  ObjectFunctional  Type Theory  52 comments  other blogs  25335 reads
The 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  10887 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  17178 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  8860 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  10845 reads

Browse archivesActive forum topics 
Recent comments
3 hours 16 min ago
3 hours 24 min ago
3 hours 27 min ago
12 hours 4 min ago
12 hours 24 min ago
18 hours 33 min ago
22 hours 30 min ago
22 hours 33 min ago
1 day 40 min ago
1 day 2 hours ago