User loginNavigation 
FunctionalKoka a function oriented language with effect inference
Koka extends the idea of using row polymorphism to encode an effect system and the relations between them. Daan Leijen is the primary researcher behind it and his research was featured previously on LtU, mainly on row polymorphism in the Morrow Language. So far there's no paper available on the language design, just the slides from a Lang.Next talk (which doesn't seem to have video available at Channel 9), but it's in the program for HOPE 2012. By Daniel Yokomizo at 20120816 05:40  Functional  Software Engineering  Type Theory  3 comments  other blogs  16114 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  11928 reads
How to Make Ad Hoc Proof Automation Less Ad HocHow to Make Ad Hoc Proof Automation Less Ad Hoc
If you've ever toyed with Coq but run into the difficulties that many encounter in trying to construct robust, comprehensible proof scripts using tactics, which manipulate the proof state and can leave you with the "ground" of the proof rather than the "figure," if you will, in addition to being fragile in the face of change, you may wish to give this a read. It frankly never would have occurred to me to try to turn Ltac scripts into lemmas at all. This is much more appealing than most other approaches to the subject I've seen. By Paul Snively at 20120622 15:41  Functional  Implementation  Logic/Declarative  Type Theory  9 comments  other blogs  7943 reads
Validating LR(1) parsers
I've always been somewhat frustrated, while studying verified compiler technology, that the scope of the effort has generally been limited to ensuring that the AST and the generated code mean the same thing, as important as that obviously is. Not enough attention has been paid, IMHO, to other compiler phases. Parsing: The Solved Problem That Isn't does a good job illuminating some of the conceptual issues that arise in attempting to take parsers seriously as functions that we would like to compose etc. while maintaining some set of properties that hold of the individuals. Perhaps this work can shed some light on possible solutions to some of those issues, in addition to being worthwhile in its own right. Note the pleasing presence of an actual implementation that's been used on the parser of a realworld language, C99. By Paul Snively at 20120618 15:15  DSL  Functional  Implementation  Theory  4 comments  other blogs  8519 reads
Programming with Algebraic Effects and HandlersProgramming with Algebraic Effects and Handlers. Andrej Bauer and Matija Pretnar, arXiv preprint.
Eff has been discussed here before, and it's nice to see some more progress and a much more complete introduction. The paper is intended for a general audience (well, a general audience of PL enthusiasts). It's quite clear and contains a wealth of examples. What does focusing tell us about language design?A blog post about CallByPushValue by Rob Simmons: What does focusing tell us about language design?
Previously on Rob's blog: Embracing and extending the Levy language; on LtU: Call by pushvalue, Levy: a Toy CallbyPushValue Language. And let me also repeat CBPV's slogan, which is one of the finest in PL advocacy: Once the fine structure has been exposed, why ignore it? By Manuel J. Simoni at 20120305 15:17  Functional  OOP  Paradigms  24 comments  other blogs  12230 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  7035 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  11510 reads
LTL types FRP
Alan Jeffrey (to appear 2012) LTL types FRP: Lineartime 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 Lineartime 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 20111114 10:48  Functional  Type Theory  35 comments  other blogs  16738 reads
Extensible Programming with FirstClass CasesExtensible Programming with FirstClass 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 firstclass cases unify objectoriented and functional paradigms on a deeper level, since they enable firstclass 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 20111030 21:41  Functional  Software Engineering  Theory  Type Theory  33 comments  other blogs  23401 reads

Browse archivesActive forum topics 
Recent comments
33 min 8 sec ago
38 min 55 sec ago
39 min 6 sec ago
41 min 13 sec ago
50 min 3 sec ago
55 min 12 sec ago
57 min 21 sec ago
1 hour 1 min ago
1 hour 5 min ago
2 hours 35 min ago