User loginNavigation 
FunctionalHow 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  7854 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  8415 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  11815 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  6958 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  11373 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  16624 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  23162 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  11580 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  13077 reads

Browse archivesActive forum topics 
Recent comments
36 min 56 sec ago
4 hours 11 min ago
6 hours 27 min ago
6 hours 34 min ago
7 hours 25 min ago
7 hours 35 min ago
7 hours 47 min ago
9 hours 55 min ago
10 hours 6 min ago
10 hours 38 min ago