Type Theory

The Essence of Data Access in Cw

The Essence of Data Access in Cw, The power is in the dot! Gavin Bierman, Erik Meijer, and Wolfram Schulte.

In this paper we concentrate on the data dimension. Our aim is to describe the essence of these extentions; by which we mean we identify, exemplify and formalize their essential features. Our tool is a small core language FCw, which is a valid subset of the full Cw language... we are able to formalize the type system and operational semantics of the data access fragments of Cw.

If you have been following the discussions here of Cw, you already know about the language features discussed here, since the paper doesn't introduce new features. If you haven't seen Cw, section 2 is a short and readable introduction.

The rest of the paper is more formal, and unless you need to prove formal results regarding Cw, might not be all that interesting. It won't hurt to keep in mind that it exists, since some of us may need something like FCw at one point or another.

Generics: The Importance of Wildcards

Martin Bravenboer writes about generic wildcards in Java, and concludes that it is unfortunate that C# will not support wildcards or a similar mechanism.

Eric Gunnerson from Microsoft replies.

I was originally a type-erasure fan, but these days I am not so sure. I hope this turns into a fruitful discussion that helps me decide...


The Java paper was mentioned on LtU before.

A type discipline for authorization policies

A type discipline for authorization policies. Cedric Fournet; Andrew D. Gordon; Sergio Maffeis

Distributed systems and applications are often expected to enforce high-level authorization policies. To this end, the code for these systems relies on lower-level 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. For a given authorization policy, we consider the problem of checking whether a cryptographic implementation complies with the policy. We formalize authorization policies by embedding logical predicates and queries within a spi-calculus. This embedding is new, simple, and general; it allows us to treat logic programs as specifications of code using secure channels, cryptography, or a combination. Moreover, we propose a new dependent type system for verifying such implementations against their policies. Using Datalog as an authorization logic, we show how to type several examples using policies and present a general schema for compiling policies.

I guess it's dependent types day around here...

Why Dependent Types Matter

Why Dependent Types Matter. Thorsten Altenkirch Conor McBride James McKinna

We exhibit the rationale behind the design of Epigram, a dependently typed programming language and interactive program development system using refinements of a well known program, merge sort, as a running example. We discuss the relationship to other proposals to introduce aspects of dependent types into functional programming languages and sketch some topics for further work in this area.

Epigram, dependent types, general reucrsion, indexed datatypes - it's all here!


TYPES Summer School 2005

The summer school, Proofs of Programs and Formalisation of Mathematics, is in Goteborg, Sweden, August 15-26.

You might still apply for a grant, but time is short!

Only a tentative program is currently available, but I suppose the topics mentioned in it will remain in the final program, and many of them are interesting, and often discussed here on LtU.


Ωmega is a new programming language by Tim Sheard which is descended from Haskell and adds new facilities for defining static type constraints, such as allowing "users to write functions at the level of types, and then use those functions in the type of functions at value level". It also has "equality qualified types". See also Programming with Static Invariants in Omega and the manual for more information. Mentioned previously (in passing) on LtU.

Barbara Partee: Reflections of a Formal Semanticist as of Feb 2005

What follows will be a very subjective and personal view, as much my own history and development in the field and how things looked through my eyes as about the development of the field itself.

This essay is a longer version of the introductory essay in (Partee 2004). The introductory essay was first written in this long form in February 2003, but had to be cut down to about half the size to fit in the book...

This essay is about natural language semantics, but you'll find old friends here: lambdas, bindings, types, quantifiers etc. If you are lazy, go directly to footnote 25...

No surprise, really, if you follow the links we give here from time to time about TLGs and such.

The Church Project

http://types.bu.edu or http://www.church-project.org

The Church Project investigates the foundations, design principles and implementation techniques of programming languages and related systems. The overall goal is the development of software technology that performs better and is more reliable. The project is named in honor of Alonzo Church, the inventor of the lambda calculus.

Four major research efforts (supported by various funding bodies including EC, EPSRC, and NSF) are presently undertaken by project participants:

  • Compiling with Flow Types
  • Compositional Analysis
  • Programming with Dependent Types (DML) (Xanadu)
  • Linear Naming and Computation

We previously linked to a document on this site, but not the site itself.

A Type System Equivalent to Flow Analysis

A Type System Equivalent to Flow Analysis
Flow-based safety analysis of higher-order languages has been studied by Shivers, and Palsberg and Schwartzbach. Open until now is the problem of finding a type system that accepts exactly the same programs as safety analysis. In this paper we prove that Amadio and Cardelli's type system with subtyping and recursive types accepts the same programs as a certain safety analysis. The proof involves mappings from types to flow information and back. As a result, we obtain an inference algorithm for the type system, thereby solving an open problem.

I believe it's instructive to see type systems in this light. Did we discuss something like this recently?

Poly* type inference tool

Poly* is a novel retargetable meta type system for various process and mobility calculi. Poly* is a direct descendant of PolyA, a type system for Mobile Ambients by Amtoft, Makholm, and Wells. Meta* is a generic process calculus that can be instantiated to specific process calculi like the Pi-calculus and Mobile Ambients by supplying reduction rules.

A web interface is available for experimentation after you can read the technical report and ESOP 2005 paper.

The list of common questions and answers about Poly* may be a good place to start if you are merely curious.

XML feed