User loginNavigation 
Type TheoryExtensible Records With Scoped Labels
Extensible Records With Scoped Labels
Daan Leijen Records provide a safe and flexible way to construct data structures. We describe a natural approach to typing polymorphic and extensible records that is simple, easy to use in practice, and straightforward to implement. A novel aspect of this work is that records can contain duplicate labels, effectively introducing a form of scoping over the labels. Furthermore, it is a fully orthogonal extension to existing type systems and programming languages...Last time one of Daan's papers was mentioned, there was a very positive response (after Frank reminded us a couple of times). This is equally good: clever, elegant, and clearly presented. (Between this and the Sheard paper, it's a good week for practical type systems...) By Matt Hellige at 20051115 16:29  Implementation  Type Theory  9 comments  other blogs  13242 reads
Putting CurryHoward to Work
via LtU forums:
The CurryHoward isomorphism states that types are propositions and that programs are proofs. This allows programmers to state and enforce invariants of programs by using types. Unfortunately, the type systems of today's functional languages cannot directly express interesting properties of programs. To alleviate this problem, we propose the addition of three new features to functional programming languages such as Haskell: Generalized Algebraic Datatypes, Extensible Kind Systems, and the generation, propagation, and discharging of Static Propositions. These three new features are backward compatible with existing features, and combine to enable a new programming paradigm for functional programmers. This paradigm makes it possible to state and enforce interesting properties of programs using the type system, and it does this in manner that leaves intact the functional programming style, known and loved by functional programmers everywhere.The paper is short and reasonably easy to read, also the examples are very realistic  check section 13 as a starter. Getting half through the paper made we willing to play with implementation, getting to the last page made my hands itching to implement my own PL with a similar type system. You are warned :) Just What is it that Makes MartinLof's Type Theory so Different, so Appealing?MartinLÃ¶f's Type Theory (MLTT) was developed by Per MartinLÃ¶f in the early 1970s, as a constructive foundation for mathematics. The theory is clear and simple. Because of this it has been used for everything from program derivation to handling donkey sentences. Yet another propositionsastypes tutorial. It seems pretty easy to follow, and it is quite short (16 pages). P.S Why all the theory on LtU these days? Because the editors who keep posting are into theory. The other editors should be nudged to start posting cool handson stuff... Linear types for aliased resources
Linear types for aliased resources. Chris Hawblitzel.
Type systems that track aliasing can verify statedependent program properties. For example, such systems can verify that a program does not access a resource after deallocating the resource. The simplest way to track aliasing is to use linear types, which on the surface appear to ban the aliasing of linear resources entirely. Since banning aliasing is considered too draconian for many practical programs, researchers have proposed type systems that allow limited forms of aliasing, without losing total control over statedependent properties. This paper describes how to encode one such system, the capability calculus, using a type system based on plain linear types with no special support for aliasing. Given welltyped capability calculus source programs, the encodings produce welltyped target programs based on linear types. These encodings demonstrate that, contrary to common expectations, linear type systems can express aliasing of linear resources. The prose is slightly confusing, but the code examples help. Sections 1 & 2 should be enough for those who only want to understand the problem with aliasing, and get a glimpse of what linear types are. By Ehud Lamm at 20051021 16:12  Software Engineering  Type Theory  30 comments  other blogs  11198 reads
NumberParameterized Types by Oleg KiselyovNumberParameterized Types by Oleg Kiselyov
Oleg shows several approaches towards encoding numbers into types and using those numbers to check list length, matching sizes for matrices or vectors. Oleg also points out connections to dependent types, phantom types, and shapeinvariant programming. A Type Discipline for Authorization Policies
Cedric Fournet; Andrew D. Gordon; Sergio Maffeis. A Type Discipline for Authorization Policies. ESOP 2005.
Distributed systems and applications are often expected to enforce highlevel authorization policies. To this end, the code for these systems relies on lowerlevel security mechanisms such as, for instance, digital signatures, local ACLs, and encrypted communications. In principle, authorization specifications can be separated from code and carefully audited. Logic programs, in particular, can express policies in a simple, abstract manner. We consider the problem of checking whether a distributed implementation based on communication channels and cryptography complies with a logical authorization policy. We formalize authorization policies and their connection to code by embedding logical predicates and claims within a process calculus. We formulate policy compliance operationally by composing a process model of the distributed system with an arbitrary opponent process. Moreover, we propose a new dependent type system for verifying policy compliance of implementation code. Using Datalog as an authorization logic, we show how to type several examples using policies and present a general schema for compiling policies. Another "extreme" use of static typing... By Ehud Lamm at 20050923 18:57  Logic/Declarative  Parallel/Distributed  Type Theory  1 comment  other blogs  8516 reads
Guarded Induction and Weakly Final Coalgebras in Dependent Type Theory
Quite a mouthful, I wonder if it would attract more people if it were titled "Interactive programming in Epigram" :)
Guarded Induction and Weakly Final Coalgebras in Dependent Type Theory In this article we are going to explore one approach to the representation of interactive programs in dependent type theory. The approach we take centres on the concept of "monadic IO" used in functional programming. We will see that in dependent type theory, besides nondependent interactive programs in which the interface between the user and the real world is fixed, as in ordinary functional programming, there is a natural notion of statedependent interactive programs, in which the interface changes over time. Automatic type inference via partial evaluation
Automatic type inference via partial evaluation. Aaron Tomb, Cormac Flanagan. PPDPâ€™05.
Type checking and type inference are fundamentally similar problems. However, the algorithms for performing the two operations, on the same type system, often differ significantly. The type checker is typically a straightforward encoding of the original type rules. For many systems, type inference is performed using a twophase, constraintbased algorithm.We present an approach that, given the original type rules written as clauses in a logic programming language, automatically generates an efficient, twophase, constraintbased type inference algorithm. Our approach works by partially evaluating the type checking rules with respect to the target program to yield a set of constraints suitable for input to an external constraint solver. This approach avoids the need to manually develop and verify a separate type inference algorithm, and is ideal for experimentation with and rapid prototyping of novel type systems. Also somewhat relevant to the discussions here about type checking as abstract interpretation. By Ehud Lamm at 20050717 10:55  Logic/Declarative  MetaProgramming  Type Theory  4 comments  other blogs  6653 reads
A Typed, Compositional Logic for a StackBased Abstract Machine
A Typed, Compositional Logic for a StackBased Abstract Machine. Nick Benton. MSRTR200584. June 2005.
We define a compositional program logic in the style of Floyd and Hoare for a simple, typed, stackbased abstract machine with unstructured control flow, global variables and mutually recursive procedure calls. Notable features of the logic include a careful treatment of auxiliary variables and quantification and the use of substructural typing to permit local, modular reasoning about program fragments. Semantic soundness is established using an interpretation of types and assertions defined by orthogonality with respect to sets of contexts. By Ehud Lamm at 20050702 09:14  Implementation  Semantics  Type Theory  2 comments  other blogs  7707 reads
A FormulaeasTypes Interpretation of Subtractive LogicA FormulaeasTypes Interpretation of Subtractive Logic
Yet another connection between subtractive logic and control. I remember the author mentioned on LtU, but I cannot find any citations. By Andris Birkmanis at 20050629 11:46  Functional  Lambda Calculus  Type Theory  1 comment  other blogs  4179 reads

Browse archivesActive forum topics 
Recent comments
6 days 1 hour ago
6 days 20 hours ago
1 week 52 min ago
1 week 1 hour ago
1 week 2 hours ago
1 week 2 hours ago
1 week 3 hours ago
1 week 3 hours ago
1 week 7 hours ago
1 week 7 hours ago