User loginNavigation 
Type TheoryHow 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  9260 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  10205 reads
Programming as collaborative referenceProgramming as collaborative reference (extended abstract and slides) by everybody's favorite PLT tag team, Oleg and Chungchieh, from the Offthebeaten track workshop affiliated with POPL 2012:
By Manuel J. Simoni at 20120204 16:48  Paradigms  Type Theory  12 comments  other blogs  9265 reads
The Algebra of Data, and the Calculus of MutationKalani Thielen's The Algebra of Data, and the Calculus of Mutation is a very good explanation of ADTs, and also scratches the surfaces of Zippers:
(hat tip to Daniel Yokomizo, who used to be an LtU member...) By Manuel J. Simoni at 20120203 15:53  Teaching & Learning  Type Theory  11 comments  other blogs  12251 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  12883 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  35798 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  18642 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  27994 reads
The SAFE Platform
A. Dehon, B. Karel, B. Montagu, B. Pierce, J. Smith, T. Knight, S. Ray, G. Sullivan, G. Malecha, G. Morrisett, R. Pollack, R. Morisset & O. Shivers. Preliminary design of the SAFE platform. In Proceedings of the 6th Workshop on Programming Languages and Operating Systems (PLOS 2011). ACM, Oct. 2011.
ABSTRACT — Safe is a cleanslate design for a secure host architecture, coupling advances in programming languages, operating systems, and hardware, and incorporating formal methods at every step. The project is still at an early stage, but we have identiï¬ed a set of fundamental architectural choices that we believe will work together to yield a highassurance system. We sketch the current state of the design and discuss several of these choices.Proving an operating system correct down to the hardware specification and against a threat model does seem to demand new programming languages and higherorder constructive type theory. By Charles Stewart at 20110912 11:41  General  Type Theory  12 comments  other blogs  10990 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  20888 reads

Browse archivesActive forum topics 
Recent comments
22 min 13 sec ago
10 hours 44 min ago
12 hours 41 min ago
20 hours 21 min ago
20 hours 24 min ago
21 hours 5 min ago
21 hours 24 min ago
1 day 5 hours ago
1 day 7 hours ago
1 day 9 hours ago