User loginNavigation 
Type TheoryThe Syntax and Semantics of Quantitative Type TheoryThe Syntax and Semantics of Quantitative Type Theory by Robert Atkey:
Resourceaware programming is a hot topic these days, with Rust exploiting affine and ownership types to scope and track resource usage, and with Ethereum requiring programs to spend "gas" to execute. Combining linear and dependent types has proven difficult though, so making it easier to track and reason about resource usage in dependent type theories would then be a huge benefit to making verification more practical in domains where resources are limited. By naasking at 20170725 17:28  Semantics  Theory  Type Theory  5 comments  other blogs  26629 reads
RustBelt: Securing the Foundations of the Rust Programming LanguageRustBelt: Securing the Foundations of the Rust Programming Language by Ralf Jung, JacquesHenri Jourdan, Robbert Krebbers, Derek Dreyer:
Rust is definitely pushing the envelope in a new direction, but there's always a little wariness around using libraries that make use of unsafe features, since "safety with performance" is a main reason people want to use Rust. So this is a great step in the right direction! By naasking at 20170710 15:14  Functional  ObjectFunctional  Type Theory  login or register to post comments  other blogs  12882 reads
Type Systems as MacrosType Systems as Macros, by Stephen Chang, Alex Knauth, Ben Greenman:
This looks pretty awesome considering it's not limited to simple typed languages, but extends all the way to System F and Fomega! Even better, they can reuse previous type systems to define new ones, thereby reducing the effort to implement more expressive type systems. All code and further details available here, and here's a blog post where Ben Greenman further discusses the related "type tailoring", and of course, these are both directly related to Active Libraries. Taken to its extreme, why not have an assembler with a powerful macro system of this sort as your host language, and every highlevel language would be built on this. I'm not sure if this approach would extend that far, but it's an interesting idea. You'd need a cpplike highly portable macro tool, and porting to a new platform consists of writing architecturespecific macros for some core language, like System F. This work may also conceptually dovetail with another thread discussing fexprs and compilation. By naasking at 20170419 23:38  DSL  Functional  Lambda Calculus  MetaProgramming  Type Theory  15 comments  other blogs  41335 reads
Contextual isomorphisms
Contextual Isomorphisms
This paper is based on a very simple idea that everyone familiar with typesystems can enjoy. It then applies it in a technical setting in which it brings a useful contribution. I suspect that many readers will find that second part too technical, but they may still enjoy the idea itself. To facilitate this, I will rephrase the abstract above in a way that I hope makes it accessible to a larger audience. The problem that the paper solves is: how do we know what it means
for two types to be equivalent? For many languages they are reasonable
definitions of equivalence (such that: there exists a bijection
between these two types in the language), but for more advanced
languages these definitions break down. For example, in presence of
hidden mutable state, one can build a pair of functions from the
oneelement type To define what it means for two program fragments to be equivalent, we have a "gold standard", which is contextual equivalence: two program fragments are contextually equivalent if we can replace one for the other in any complete program without changing its behavior. This is simple to state, it is usually clear how to instantiate this definition for a new system, and it gives you a satisfying notion of equivalent. It may not be the most convenient one to work with, so people define others, more specific notions of equivalence (typically betaetaequivalence or logical relations); it is fine if they are more sophisticated, and their definiton harder to justify or understand, because they can always be compared to this simple definition to gain confidence. The simple idea in the paper above is to use this exact same trick to define what it means for two types to be equivalent. Naively, one could say that two types are equivalent if, in any welltyped program, one can replace some occurrences of the first type by occurrences of the second type, all other things being unchanged. This does not quite work, as changing the types that appear in a program without changing its terms would create illtyped terms. So instead, the paper proposes that two types are equivalent when we are told how to transform any program using the first type into a program using the second type, in a way that is bijective (invertible) and compositional  see the paper for details. Then, the author can validate this definition by showing that, when instantiated to languages (simple or complex) where existing notions of equivalence have been proposed, this new notion of equivalence corresponds to the previous notions. (Readers may find that even the warmup part of the paper, namely the sections 1 to 4, pages 1 to 6, are rather dense, with a compactly exposed general idea and arguably a lack of concrete examples that would help understanding. Surely this terseness is in large part a consequence of strict page limits  conference articles are the tweets of computer science research. A nice sideeffect (no pun intended) is that you can observe a carefully chosen formal language at work, designed to expose the setting and perform relevant proofs in minimal space: category theory, and in particular the concept of naturality, is the killer spacesaving measure here.) Polymorphism, subtyping and type inference in MLsubI am very enthusiastic about the following paper: it brings new ideas and solves a problem that I did not expect to be solvable, namely usable type inference when both polymorphism and subtyping are implicit. (By "usable" here I mean that the inferred types are both compact and principal, while previous work generally had only one of those properties.)
Polymorphism, Subtyping, and Type Inference in MLsub
The paper is full of interesting ideas. For example, one idea is that adding type variables to the base grammar of types  instead of defining them by their substitution  forces us to look at our type systems in ways that are more open to extension with new features. I would recommend looking at this paper even if you are interested in ML and type inference, but not subtyping, or in polymorphism and subtyping, but not type inference, or in subtyping and type inference, but not functional languages. This paper is also a teaser for the first's author PhD thesis, Algebraic Subtyping. There is also an implementation available. (If you are looking for interesting work on inference of polymorphism and subtyping in objectoriented languages, I would recommend Getting FBounded Polymorphism into Shape by Ben Greenman, Fabian Muehlboeck and Ross Tate, 2014.) Proving Programs Correct Using Plain Old Java TypesProving Programs Correct Using Plain Old Java Types, by Radha Jagadeesan, Alan Jeffrey, Corin Pitcher, James Riely:
Not a new paper, but it provides a lightweight verification technique for some program properties that you can use right now, without waiting for integrated theorem provers or SMT solvers. Properties that require only monotone typestates can be verified, ie. those that operations can only move the typestate "forwards". In order to achieve this, they require programmers to follow a few simple rules to avoid Java's pervasive nulls. These are roughly: don't assign null explicitly, be sure to initialize all fields when constructing objects. Fully Abstract Compilation via Universal EmbeddingFully Abstract Compilation via Universal Embedding by Max S. New, William J. Bowman, and Amal Ahmed:
Potentially a promising step forward to secure multilanguage runtimes. We've previously discussed security vulnerabilities caused by full abstraction failures here and here. The paper also provides a comprehensive review of associated literature, like various means of protection, back translations, embeddings, etc. By naasking at 20160727 15:57  Lambda Calculus  Semantics  Theory  Type Theory  5 comments  other blogs  41215 reads
SetTheoretic Types for Polymorphic VariantsSetTheoretic Types for Polymorphic Variants by Giuseppe Castagna, Tommaso Petrucciani, and Kim Nguyễn:
Looks like a nice result. They integrate union types and restricted intersection types for complete type inference, which prior work on CDuce could not do. The disadvantage is that it does not admit principal types, and so inference is nondeterministic (see section 5.3.2). No value restriction is needed for algebraic effects and handlersNo value restriction is needed for algebraic effects and handlers, by Ohad Kammar and Matija Pretnar:
Looks like a nice integration of algebraic effects with simple HindlyMilner, but which yields some unintuitive conclusions. At least I certainly found the possibility of supporting dynamically scoped state but not reference cells surprising! It highlights the need for some future work to support true reference cells, namely a polymorphic type and effect system to generate fresh instances. By naasking at 20160525 13:54  Effects  Functional  Type Theory  login or register to post comments  other blogs  24582 reads
Type Checking Modular Multiple Dispatch with Parametric Polymorphism and Multiple InheritanceType Checking Modular Multiple Dispatch with Parametric Polymorphism and Multiple Inheritance by Eric Allen, Justin Hilburn, Scott Kilpatrick, Victor Luchangco, Sukyoung Ryu, David Chase, Guy L. Steele Jr.:
Fortress was briefly covered here a couple of times, as were multimethods and multiple dispatch, but this paper really generalizes and nicely summarizes previous work on statically typed modular multimethods, and does a good job explaining the typing rules in an accessible way. The integration with parametric polymorphism I think is key to applying multimethods in other domains which may want modular multimethods, but not multiple inheritance. The Formalization in COQ might also be of interest to some. Also, another interesting point is Fortress' use of secondclass intersection and union types to simplify type checking. By naasking at 20160401 01:25  ObjectFunctional  Theory  Type Theory  36 comments  other blogs  25417 reads

Browse archivesActive forum topics 
Recent comments
2 weeks 2 days ago
2 weeks 2 days ago
2 weeks 3 days ago
2 weeks 3 days ago
2 weeks 3 days ago
2 weeks 3 days ago
2 weeks 5 days ago
3 weeks 52 min ago
3 weeks 4 days ago
3 weeks 5 days ago