## User login## Navigation |
## Type Theory## 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 2016-07-27 15:57 | Lambda Calculus | Semantics | Theory | Type Theory | 5 comments | other blogs | 42710 reads
## Set-Theoretic Types for Polymorphic VariantsSet-Theoretic 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 non-deterministic (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 Hindly-Milner, 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 2016-05-25 13:54 | Effects | Functional | Type Theory | login or register to post comments | other blogs | 25092 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 second-class intersection and union types to simplify type checking. By naasking at 2016-04-01 01:25 | Object-Functional | Theory | Type Theory | 36 comments | other blogs | 26619 reads
## Breaking Through the Normalization Barrier: A Self-Interpreter for F-omegaBreaking Through the Normalization Barrier: A Self-Interpreter for F-omega, by Matt Brown and Jens Palsberg:
I haven't gone through the whole paper, but their claims are compelling. They have created self-interpreters 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 non-typesafe runtime features, into type safe libraries. By naasking at 2015-11-10 14:23 | Functional | Theory | Type Theory | 24 comments | other blogs | 21342 reads
## Dependent Types for Low-Level ProgrammingDependent Types for Low-Level 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. flow-insensitive checking introduces runtime assertions using these locals, 3. flow-sensitive 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 special-cased monad transformers against this new formulation of extensible effects using Freer monads. See also the reddit discussion. By naasking at 2015-09-05 14:30 | Functional | Theory | Type Theory | 18 comments | other blogs | 16272 reads
## Self-Representation in Girard’s System USelf-Representation in Girard’s System U, by Matt Brown and Jens Palsberg:
Typed self-representation has come up here on LtU in the past. I believe the best self-interpreter available prior to this work was a variant of Barry Jay's SF-calculus, covered in the paper Typed Self-Interpretation by Pattern Matching (and more fully developed in Structural Types for the Factorisation Calculus). These covered statically typed self-interpreters without resorting to undecidable type:type rules. However, being combinator calculi, they're not very similar to most of our programming languages, and so self-interpretation was still an active problem. Enter Girard's System U, which features a more familiar type system with only kind * and kind-polymorphic types. However, System U is not strongly normalizing and is inconsistent as a logic. Whether self-interpretation can be achieved in a strongly normalizing language with decidable type checking is still an open problem. By naasking at 2015-06-11 18:45 | Functional | Lambda Calculus | Theory | Type Theory | 28 comments | other blogs | 12915 reads
## Second-order logic explained in plain EnglishJohn Corcoran, Second-order logic explained in plain English, in There is something a little bit Guy Steele-ish about trying to explain the fundamentals of second-order logic (SOL, the logic that Quine branded as set theory in sheep's clothing) and its model theory while avoiding any formalisation. This paper introduces the ideas of SOL via looking at logics with finite, countable and uncountable models, and then talks about FOL and SOL as being complementary approaches to axiomatisation that are each deficient by themself. He ends with a plea for SOL as being an essential tool at least as a heuristic. |
## Browse archives## Active forum topics |

## Recent comments

2 hours 11 min ago

5 hours 31 min ago

5 hours 47 min ago

10 hours 17 min ago

17 hours 35 min ago

23 hours 6 min ago

23 hours 14 min ago

1 day 3 hours ago

1 day 21 hours ago

1 day 23 hours ago