## User login## Navigation |
## Functional## 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 2012-01-28 15:57 | Functional | Lambda Calculus | Semantics | Type Theory | 16 comments | other blogs | 10688 reads
## LTL types FRP
Alan Jeffrey (to appear 2012) LTL types FRP: Linear-time Temporal Logic Propositions as Types, Proofs as Functional Reactive Programs. To be presented at next year's
Programming Languages meets Program Verification, (PLPV 2012).
Functional Reactive Programming (FRP) is a form of reactive programming whose model is pure functions over signals. FRP is often expressed in terms of arrows with loops, which is the type class for a Freyd category (that is a premonoidal category with a cartesian centre) equipped with a premonoidal trace. This type system sufï¬ces to deï¬ne the dataï¬‚ow structure of a reactive program, but does not express its temporal properties. In this paper, we show that Linear-time Temporal Logic (LTL) is a natural extension of the type system for FRP, which constrains the temporal behaviour of reactive programs. We show that a constructive LTL can be deï¬ned in a dependently typed functional language, and that reactive programs form proofs of constructive LTL properties. In particular, implication in LTL gives rise to stateless functions on streams, and the â€œconstrainsâ€ modality gives rise to causal functions. We show that reactive programs form a partially traced monoidal category, and hence can be given as a form of arrows with loops, where the type system enforces that only decoupled functions can be looped.Via Alan's G+ feed. By Charles Stewart at 2011-11-14 10:48 | Functional | Type Theory | 35 comments | other blogs | 15935 reads
## Extensible Programming with First-Class CasesExtensible Programming with First-Class Cases, by Matthias Blume, Umut A. Acar, and Wonseok Chae:
This is an elegant solution to the expression problem for languages with pattern matching. This paper was posted twice in LtU comments, but it definitely deserves its own story. Previous solutions to the exression problem are rather more involved, like Garrigue's use of recursion and polymorphic variants, because they lack support for extensible records which makes this solution so elegant. Extensible records and first-class cases unify object-oriented and functional paradigms on a deeper level, since they enable first-class messages to be directly encoded. Add a sensible system for dynamics, and I argue you have most of the power people claim of dynamic languages without sacrificing the safety of static typing. By naasking at 2011-10-30 21:41 | Functional | Software Engineering | Theory | Type Theory | 33 comments | other blogs | 21966 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 Curry-Howard 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).
By Paul Snively at 2011-10-30 16:05 | Functional | Lambda Calculus | Logic/Declarative | Semantics | 32 comments | other blogs | 11061 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 2011-09-10 20:25 | DSL | Fun | Functional | Paradigms | Semantics | Theory | 5 comments | other blogs | 12583 reads
## OpaOpa is a new member in the family of languages aiming to make web programming transparent by automatically generating client-side Javascript and handling communication and session control. Opa is written in OCaml. A hierarchical database and web server are integrated with the language. The distribution model is based on a notion of a session, a construct roughly comparable to process definitions in the join-calculus or to concurrent objects in a number of formalisms. A good place to start is here. And here you can find several example programs with accompanying source code. By Ehud Lamm at 2011-08-25 16:29 | Functional | Parallel/Distributed | 66 comments | other blogs | 47644 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 type-directed partial evaluation, but that's literally another story). By Paul Snively at 2011-07-28 18:11 | Category Theory | Functional | Implementation | Semantics | Type Theory | 35 comments | other blogs | 12376 reads
## Levy: a Toy Call-by-Push-Value 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 hands-on 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 2011-07-14 18:57 | Fun | Functional | Implementation | Lambda Calculus | Paradigms | Semantics | Teaching & Learning | Theory | 4 comments | other blogs | 17508 reads
## Kleisli Arrows of Outrageous FortuneKleisli Arrows of Outrageous Fortune
I discovered this Googling around in an attempt to find some decent introductory material to Kleisli arrows. This isn't introductory, but it's a good resource. :-) The good introductory material I found was this. By Paul Snively at 2011-05-14 15:19 | Category Theory | Functional | Type Theory | 6 comments | other blogs | 10464 reads
## Patterns in Functional ProgrammingThe good news is that Jeremy Gibbons is writing a book on Patterns in Functional Programming. Even better news is that he is blogging about it as he goes along! Those unfamiliar with the topic may want to begin at the beginning, though I personally just rummaged around. Some may enjoy going to the papers rather than the blog, or even better to the LtU discussions about many of them. Alternatively, I think it might be a great opportunity to ask Jeremy questions using the comments on his blog. I am sure this can be a very productive learning experience, and will surely help the book! |
## Browse archives## Active forum topics |

## Recent comments

39 min 2 sec ago

59 min 42 sec ago

1 hour 9 min ago

3 hours 3 min ago

6 hours 33 min ago

9 hours 18 min ago

9 hours 41 min ago

10 hours 57 sec ago

11 hours 22 min ago

13 hours 30 min ago