User loginNavigation 
Type TheoryA 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  7882 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  4283 reads
Generics are a mistake?Generics Considered HarmfulKen Arnold, "programmer and author who helped create Jini, JavaSpaces, Curses, and Rogue", writes that the usefulness of generics is outweighed by their complexity. Ken is talking about Java 5, but such critiques are wellknown for C++, and C# is not immune either. Ken describes the Java case as follows:
The article contains a few simple supporting examples, including the interesting definition of Java 5's Enum<T extends Enum<T>> ...which "we're assured by the type theorists ... we should simply not think about too much, for which we are grateful." If we accept the article's premise, here's a question with an LtU spin: do the more elegant, tractable polymorphic inferencing type systems, as found in functional languages, improve on this situation enough to be a viable alternative that could address these complexity problems? In other words, are these problems a selling point for better type systems, or another barrier to adoption? [Thanks to Perry Metzger for the pointer.] By Anton van Straaten at 20050628 03:37  OOP  Type Theory  51 comments  other blogs  27572 reads
TypeCase: A Design Pattern for TypeIndexed Functions
Bruno C. d. S. Oliveira and Jeremy Gibbons. TypeCase: A Design Pattern for TypeIndexed Functions. Submitted for publication, June 2005.
A typeindexed function is a function that is defined for each member of some family of types. Haskell's type class mechanism provides open typeindexed functions, in which the indexing family can be extended at any time by defining a new type class instance. The purpose of this paper is to present TypeCase: a design pattern that allows the definition of closed typeindexed functions. It is inspired by Cheney and Hinze's work on lightweight approaches to generic programming. We generalise their techniques as a design pattern. Furthermore, we show that typeindexed functions with typeindexed types, and consequently generic functions with generic types, can also be encoded in a lightweight manner, thereby overcoming one of the main limitations of the lightweight approaches. A new paper in a field we follow quite closely (i.e., generic programming). The paper starts with a useful summary of important previous results, which is worth reading even if you don't plan on studying the whole paper. By Ehud Lamm at 20050620 19:37  Functional  Software Engineering  Type Theory  1 comment  other blogs  8615 reads
From shift and reset to polarized linear logic
By now, shift/reset should be as popular as call/cc was ten years ago. Some think these control operators are even more important in practice than call/cc, and should be directly supported by PLs. I believe, this paper by Chungchieh Shan will be interesting to many who loves logic and CurryHoward isomorphism.
From shift and reset to polarized linear logic Abstract: Griffin pointed out that, just as the pure lambdacalculus corresponds to intuitionistic logic, a lambdacalculus with firstclass continuations corresponds to classical logic. We study how firstclass delimited continuations, in the form of Danvy and Filinskiâ€™s shift and reset operators, can also be logically interpreted. First, we refine Danvy and Filinskiâ€™s type system for shift and reset to distinguish between pure and impure functions. This refinement not only paves the way for answer type polymorphism, which makes more terms typable, but also helps us invert the continuationpassingstyle (CPS) transform: any pure lambdaterm with an appropriate type is betaetaequivalent to the CPS transform of some shiftreset expression. We conclude that the lambdacalculus with shift and reset and the pure lambdacalculus have the same logical interpretation, namely good old intuitionistic logic. Second, we mix delimited continuations with undelimited ones. Informed by the preceding conclusion, we translate the lambdacalculus with shift and reset into a polarized variant of linear logic that integrates classical and intuitionistic reasoning. Extending previous work on the lambdaÂµcalculus, this unifying intermediate language expresses computations with and without control effects, on delimited and undelimited continuations, in callbyvalue and callbyname settings. By Andris Birkmanis at 20050606 19:17  Functional  Lambda Calculus  Semantics  Type Theory  15 comments  other blogs  9886 reads
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. By Ehud Lamm at 20050528 09:07  Semantics  Type Theory  XML  login or register to post comments  other blogs  6127 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  11589 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  3815 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  3643 reads

Browse archivesActive forum topicsNew forum topics 
Recent comments
1 week 10 hours ago
1 week 3 days ago
1 week 3 days ago
1 week 4 days ago
1 week 4 days ago
1 week 4 days ago
1 week 5 days ago
1 week 5 days ago
1 week 5 days ago
1 week 5 days ago