User loginNavigation 
SemanticsLuca Cardelli FestschriftEarlier this week Microsoft Research Cambridge organised a Festschrift for Luca Cardelli. The preface from the book:
Hopefully the videos will be posted soon. By Ohad Kammar at 20140912 10:10  Category Theory  Lambda Calculus  Misc Books  Semantics  Theory  Type Theory  4 comments  other blogs  2989 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  10927 reads
Milner Symposium 2012The Milner Symposium 2012 was held in Edinburgh this April in memory of the late Robin Milner.
The programme consisted of academic talks by colleagues and past students. The talks and slides are available online. I particularly liked the interleaving of the personal and human narrative underlying the scientific journey. A particularly good example is Joachim Parrow's talk on the origins of the pi calculus. Of particular interest to LtU members is the panel on the future of functional programming languages, consisting of Phil Wadler, Xavier Leroy, David MacQueen, Martin Odersky, Simon PeytonJones, and Don Syme. By Ohad Kammar at 20121016 17:31  Functional  General  History  Parallel/Distributed  Semantics  Theory  3 comments  other blogs  11872 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  10626 reads
Tool Demo: ScalaVirtualized
Scala has always had a quite good EDSL story thanks to implicits, dot and pareninference, and methodsasoperators. Lately there are proposals to provide it with both macrosinthecamlp4sense and support for multistage programming. This paper goes into some depth on the foundations of the latter subject. By Paul Snively at 20120526 22:28  DSL  Implementation  MetaProgramming  ObjectFunctional  Scala  Semantics  Type Theory  login or register to post comments  other blogs  7809 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  10579 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  10999 reads
A Semantic Model for Graphical User InterfacesNick Benton and Neel Krishnaswami, ICFP'11, A Semantic Model for Graphical User Interfaces:
This is an application of their (more squiggly) LICS'11 submission, Ultrametric Semantics of Reactive Programs. In both these cases, I find appealing the fact the semantic model led to a type system and a language that was tricky to find. By Ohad Kammar at 20110910 20:25  DSL  Fun  Functional  Paradigms  Semantics  Theory  5 comments  other blogs  12528 reads
Lightweight Monadic Programming in MLLightweight Monadic Programming in ML
This is an intriguing paper, with an implementation in about 2,000 lines of OCaml. I'm especially interested in its application to probabilistic computing, yielding a result related to Kiselyov and Shan's Hansei effort, but without requiring delimited continuations (not that there's anything wrong with delimited continuations). On a theoretical level, it's nice to see such a compelling example of what can be done once types are freed from the shackle of "describing how bits are laid out in memory" (another such compelling example, IMHO, is typedirected partial evaluation, but that's literally another story). By Paul Snively at 20110728 18:11  Category Theory  Functional  Implementation  Semantics  Type Theory  35 comments  other blogs  12212 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  17366 reads

Browse archivesActive forum topics 
Recent comments
22 hours 50 min ago
1 day 13 hours ago
2 days 48 min ago
3 days 15 hours ago
3 days 22 hours ago
3 days 23 hours ago
4 days 1 hour ago
4 days 1 hour ago
4 days 2 hours ago
4 days 2 hours ago