User loginNavigation 
Type TheoryContextual 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  36202 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  Functional  Type Theory  login or register to post comments  other blogs  23576 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  24169 reads
Breaking Through the Normalization Barrier: A SelfInterpreter for FomegaBreaking Through the Normalization Barrier: A SelfInterpreter for Fomega, by Matt Brown and Jens Palsberg:
I haven't gone through the whole paper, but their claims are compelling. They have created selfinterpreters in System F, System Fω and System Fω+, which are all strongly normalizing typed languages. Previously, the only instance of this for a typed language was Girard's System U, which is not strongly normalizing. The key lynchpin appears in this paragraph on page 2:
Pretty cool if this isn't too complicated in any given language. Could let one move some previously nontypesafe runtime features, into type safe libraries. By naasking at 20151110 14:23  Functional  Theory  Type Theory  24 comments  other blogs  18248 reads
Dependent Types for LowLevel ProgrammingDependent Types for LowLevel Programming by Jeremy Condit, Matthew Harren, Zachary Anderson, David Gay, and George C. Necula:
A conceptually simple approach to verifying the safety of C programs, which proceeeds in 3 phases: 1. infer locals that hold pointer bounds, 2. flowinsensitive checking introduces runtime assertions using these locals, 3. flowsensitive optimization that removes the assertions that it can prove always hold. You're left with a program that ensures runtime safety with as few runtime checks as possible, and the resulting C program is compiled with gcc which can perform its own optimizations. This work is from 2007, and the project grew into the Ivy language, which is a C dialect that is fully backwards compatible with C if you #include a small header file that includes the extensions. It's application to C probably won't get much uptake at this point, but I can see this as a useful compiler plugin to verify unsafe Rust code. Freer Monads, More Extensible EffectsFreer Monads, More Extensible Effects, by Oleg Kiselyov and Hiromi Ishii:
This looks very promising, and includes some benchmarks comparing the heavily optimized and specialcased monad transformers against this new formulation of extensible effects using Freer monads. See also the reddit discussion. By naasking at 20150905 14:30  Functional  Theory  Type Theory  18 comments  other blogs  13789 reads

Browse archivesActive forum topics 
Recent comments
11 hours 28 min ago
23 hours 48 min ago
1 day 11 hours ago
1 day 12 hours ago
1 day 13 hours ago
1 day 14 hours ago
1 day 14 hours ago
2 days 21 hours ago
2 days 22 hours ago
3 days 2 min ago