User loginNavigation |
Type TheoryVellvm: 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 | 15234 reads
Deca, an LtU-friendly bare metal systems programming languageThe Deca programming language is "a language designed to provide the advanced features of sophisticated, high-level programming languages while still programming as close as possible to the bare metal. It brings in the functional, object-oriented, 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 region-and-effect system that prohibits unsafe escaping pointers and double-free 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 2012-01-02 02:40 | Implementation | Lambda Calculus | Object-Functional | Type Theory | 52 comments | other blogs | 43874 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 dataflow 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 | 22229 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 | 41319 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 clean-slate 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 high-assurance 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 higher-order constructive type theory. By Charles Stewart at 2011-09-12 11:41 | General | Type Theory | 12 comments | other blogs | 13175 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 | 25633 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 | 17212 reads
Asynchronous Proof Processing with Isabelle/Scala and Isabelle/jEditAsynchronous Proof Processing with Isabelle/Scala and Isabelle/jEdit. Makarius Wenzel, UITP 2010.
I thought this was a nice paper on the pragmatics of incremental, interactive proof editing. I've suspected for a while that as programming languages and IDEs grow more sophisticated and do more computationally-intensive checks at compile time (including but not limited to theorem proving), it will become similarly important to design our languages to support modular and incremental analysis. However, IDE designs also need more experimentation, and unfortunately the choice of IDEs to extend seem to be limited to archaic systems like Emacs or industrial behemoths like Eclipse or Visual Studio, both of which constrain the scope for new design -- Emacs is too limited, and the API surface of Eclipse/VS is just too big and irregular. (Agda-mode for Emacs is a heroic but somewhat terrifying piece of elisp.) By neelk at 2011-04-22 15:06 | Implementation | Software Engineering | Type Theory | 4 comments | other blogs | 13464 reads
Type-checking Modular Multiple Dispatch with Parametric Polymorphism and Multiple InheritanceType-checking Modular Multiple Dispatch with Parametric Polymorphism and Multiple Inheritance. Eric Allen, Justin Hilburn, Scott Kilpatrick, Sukyoung Ryu, David Chase, Victor Luchangco, and Guy L. Steele Jr. Submitted for publication, December 2010.
So it's Sunday, and I'm researching the interaction of multiple dispatch, type-checking, and parametric polymorphism, when Google spits out this new paper by the Fortress team. Scott Kilpatrick's Master's Thesis Ad Hoc: Overloading and Language Design puts it into perspective:
All of this is a bit over my head, unfortunately, but I find it very interesting nevertheless. And it's heartening that the somewhat neglected multiple dispatch (and multiple inheritance!) is further developed by such a high caliber team. By Manuel J. Simoni at 2011-03-20 16:28 | Paradigms | Type Theory | 6 comments | other blogs | 12233 reads
The Triumph of Types: Principia Mathematica's Impact on Computer Science
The Triumph of Types: Principia Mathematica's Impact on Computer Science. Robert L. Constable
The role the ideas of Principia Mathematica played in type theory in programming languages is often alluded to in our discussions, making this contribution to a meeting celebrating the hundredth anniversary of Whitehead-and-Russell's opus provocative. To get your juices going here is a quote from page 3:
...I will discuss later our efforts at Cornell to create one such type theory, Computational Type Theory (CTT), very closely related to two others, the Calculus of Inductive Constructions (CIC) implemented in the Coq prover and widely used, and Intuitionistic Type Theory (ITT) implemented in the Alf and Agda provers. All three of these efforts, but especially CTT and ITT, were strongly influenced by Principia and the work of Bishop presented in his book Foundations of Constructive Analysis. |
Browse archives
Active forum topics
|
Recent comments
15 weeks 16 hours ago
19 weeks 2 days ago
20 weeks 6 days ago
20 weeks 6 days ago
23 weeks 4 days ago
28 weeks 2 days ago
28 weeks 2 days ago
28 weeks 5 days ago
28 weeks 5 days ago
31 weeks 3 days ago