User loginNavigation 
Lambda CalculusCost semantics for functional languagesThere is an ongoing discussion in LtU (there, and there) on whether RAM and other machine models are inherently a better basis to reason about (time and) memory usage than lambdacalculus and functional languages. Guy Blelloch and his colleagues have been doing very important work on this question that seems to have escaped LtU's notice so far. A portion of the functional programming community has long been of the opinion that we do not need to refer to machines of the Turing tradition to reason about execution of functional programs. Dynamic semantics (which are often perceived as more abstract and elegant) are adequate, selfcontained descriptions of computational behavior, which we can elevate to the status of (functional) machine model  just like "abstract machines" can be seen as just machines. This opinion has been made scientifically precise by various brands of work, including for example implicit (computational) complexity, resource analysis and cost semantics for functional languages. Guy Blelloch developed a family of cost semantics, which correspond to annotations of operational semantics of functional languages with new information that captures more intentional behavior of the computation: not only the result, but also running time, memory usage, degree of parallelism and, more recently, interaction with a memory cache. Cost semantics are selfcontained way to think of the efficiency of functional programs; they can of course be put in correspondence with existing machine models, and Blelloch and his colleagues have proved a vast amount of twoway correspondences, with the occasional extra logarithmic overhead  or, from another point of view, provided probably costeffective implementations of functional languages in imperative languages and conversely. This topic has been discussed by Robert Harper in two blog posts, Language and Machines which develops the general argument, and a second post on recent joint work by Guy and him on integrating cacheefficiency into the model. Harper also presents various cost semantics (called "cost dynamics") in his book "Practical Foundations for Programming Languages". In chronological order, three papers that are representative of the evolution of this work are the following. Parallelism In Sequential Functional Languages
Space Profiling for Functional Programs This paper clearly defines a notion of ideal memory usage (the set of store locations that are referenced by a value or an ongoing computation) that is highly reminiscent of garbage collection specifications, but without making any reference to an actual garbage collection implementation.
Cache and I/O efficient functional algorithms The cost semantics in this last work incorporates more notions from garbage collection, to reason about cacheefficient allocation of values  in that it relies on work on formalizing garbage collection that has been mentioned on LtU before.
By gasche at 20140814 11:53  Implementation  Lambda Calculus  33 comments  other blogs  31557 reads
Pure 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  20421 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  14700 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  13495 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  7981 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  12471 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  34375 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  12607 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  31119 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  10439 reads

Browse archivesActive forum topics 
Recent comments
6 hours 11 min ago
6 hours 39 min ago
8 hours 41 min ago
12 hours 8 min ago
19 hours 25 min ago
20 hours 51 min ago
1 day 8 hours ago
1 day 8 hours ago
1 day 9 hours ago
2 days 5 hours ago