## User login## Navigation |
## Type Theory## 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 | 33 comments | other blogs | 11510 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 | 14816 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 | 11790 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 | 9492 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. ## The Next Stage of StagingThe Next Stage of Staging, by Jun Inoue, Oleg Kiselyov, Yukiyoshi Kameyama:
A position paper describing the next logical progression of staging to metaprogramming over types. Now with the true first-class modules of 1ML, perhaps there's a clearer way forward. By naasking at 2015-03-29 13:34 | Functional | Meta-Programming | Theory | Type Theory | 57 comments | other blogs | 13591 reads
## Conservation laws for free!In this year's POPL, Bob Atkey made a splash by showing how to get from parametricity to conservation laws, via Noether's theorem:
By Ohad Kammar at 2014-10-28 07:52 | Category Theory | Fun | Functional | Lambda Calculus | Scientific Programming | Semantics | Theory | Type Theory | 5 comments | other blogs | 14718 reads
## Luca Cardelli FestschriftEarlier this week Microsoft Research Cambridge organised a Festschrift for Luca Cardelli. The preface from the book:
Hopefully the videos will be posted soon. By Ohad Kammar at 2014-09-12 10:10 | Category Theory | Lambda Calculus | Misc Books | Semantics | Theory | Type Theory | 4 comments | other blogs | 6173 reads
## Howard on Curry-HowardPhilip Wadler posts his exchange with William Howard on history of the Curry-Howard correspondence. Howard on Curry-Howard. |
## Browse archives## Active forum topics |

## Recent comments

1 day 9 hours ago

1 day 10 hours ago

1 day 11 hours ago

4 days 13 hours ago

5 days 3 hours ago

6 days 6 hours ago

6 days 9 hours ago

6 days 9 hours ago

6 days 10 hours ago

6 days 12 hours ago