User loginNavigation 
Type TheoryThe Gentle Art of Levitation
The Gentle Art of Levitation
2010 by James Chapman, PierreEvariste Dagand, Conor McBride, Peter Morrisy We present a closed dependent type theory whose inductive types are given not by a scheme for generative declarations, but by encoding in a universe. Each inductive datatype arises by interpreting its description—a firstclass value in a datatype of descriptions. Moreover, the latter itself has a description. Datatypegeneric programming thus becomes ordinary programming. We show some of the resulting generic operations and deploy them in particular, useful ways on the datatype of datatype descriptions itself. Surprisingly this apparently selfsupporting setup is achievable without paradox or infinite regress.It's datatype descriptions all the way down. By Andris Birkmanis at 20180511 19:26  Semantics  Type Theory  1 comment  other blogs  4225 reads
Comprehending Ringads
Comprehending Ringads
2016 by Jeremy Gibbons Ringad comprehensions represent a convenient notation for expressing database queries. The ringad structure alone does not provide a good explanation or an efficient implementation of relational joins; but by allowing heterogeneous comprehensions, involving both bag and indexed table ringads, we show how to accommodate these too.Indexed/parametric/graded monads are the key (read the paper to understand the pun). By Andris Birkmanis at 20180505 02:59  Category Theory  Semantics  Type Theory  login or register to post comments  other blogs  5348 reads
Sequent Calculus as a Compiler Intermediate LanguageSequent Calculus as a Compiler Intermediate Language
By Andris Birkmanis at 20180402 17:06  Functional  General  Lambda Calculus  Semantics  Type Theory  2 comments  other blogs  11898 reads
The 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  27119 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  13268 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  42679 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  42074 reads

Browse archivesActive forum topics 
Recent comments
6 hours 50 min ago
4 days 1 hour ago
4 days 7 hours ago
4 days 9 hours ago
4 days 19 hours ago
6 days 14 hours ago
1 week 22 hours ago
1 week 22 hours ago
1 week 2 days ago
1 week 3 days ago