User loginNavigation 
Type TheoryThe 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. By Ehud Lamm at 20050528 09:07  Semantics  Type Theory  XML  login or register to post comments  other blogs  5905 reads
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 typeerasure fan, but these days I am not so sure. I hope this turns into a fruitful discussion that helps me decide... P.S The Java paper was mentioned on LtU before. By Ehud Lamm at 20050526 20:05  Software Engineering  Type Theory  14 comments  other blogs  11109 reads
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 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. 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 spicalculus. 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... By Ehud Lamm at 20050510 19:51  Logic/Declarative  Parallel/Distributed  Type Theory  login or register to post comments  other blogs  3661 reads
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! Enjoy. TYPES Summer School 2005
The summer school, Proofs of Programs and Formalisation of Mathematics, is in Goteborg, Sweden, August 1526.
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. By Ehud Lamm at 20050510 08:06  Type Theory  login or register to post comments  other blogs  3481 reads
OmegaΩ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. By Bryn Keller at 20050407 21:24  Functional  Implementation  MetaProgramming  Type Theory  6 comments  other blogs  7476 reads
Barbara Partee: Reflections of a Formal Semanticist as of Feb 2005What 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 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. By Ehud Lamm at 20050215 10:37  History  Lambda Calculus  Semantics  Type Theory  5 comments  other blogs  9139 reads
The Church Project
http://types.bu.edu or http://www.churchproject.org
We previously linked to a document on this site, but not the site itself. By Andris Birkmanis at 20050208 17:24  Lambda Calculus  Type Theory  3 comments  other blogs  4822 reads
A Type System Equivalent to Flow Analysis
A Type System Equivalent to Flow Analysis
Flowbased safety analysis of higherorder 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 toolPoly* 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 Picalculus 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. By Ehud Lamm at 20050127 13:29  Type Theory  login or register to post comments  other blogs  3920 reads

Browse archivesActive forum topics 
Recent comments
56 min 14 sec ago
1 hour 28 min ago
4 hours 32 min ago
4 hours 58 min ago
6 hours 19 min ago
6 hours 24 min ago
6 hours 54 min ago
11 hours 51 min ago
11 hours 51 min ago
12 hours 2 min ago