## User login## Navigation |
## Theory## 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 | 6584 reads
## Cakes, Custard, and Category TheoryEugenia Cheng's new popular coscience book is out, in the U.K. under the title Cakes, Custard and Category Theory: Easy recipes for understanding complex maths, and in the U.S. under the title How to Bake Pi: An Edible Exploration of the Mathematics of Mathematics:
Cheng, one of the Catsters, gives a guided tour of mathematical thinking and research activities, and through the core philosophy underlying category theory. This is the kind of book you can give to your grandma and grandpa so they can boast to their friends what her grandchildren are doing (and bake you a nice dessert when you come and visit :) ). A pleasant weekend reading. By Ohad Kammar at 2015-07-17 16:47 | Category Theory | Critiques | Fun | General | Semantics | Theory | login or register to post comments | other blogs | 3971 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 | 6383 reads
## 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 | 11325 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 | 13938 reads
## Seemingly impossible programsIn case this one went under the radar, at POPL'12, Martín Escardó gave a tutorial on seemingly impossible functional programs:
A shorter version (coded in Haskell) appears in Andrej Bauer's blog. By Ohad Kammar at 2014-10-22 09:57 | Category Theory | Fun | Functional | Paradigms | Semantics | Theory | 36 comments | other blogs | 13107 reads
## sml-family.orgIn his blog, Bob Harper, in joint effort with Dave MacQueen and Lars Bergstrom, announces the launch of sml-family.org:
By Ohad Kammar at 2014-09-30 19:27 | Fun | Functional | History | Implementation | Paradigms | Semantics | Theory | 1 comment | other blogs | 8206 reads
## Inferring algebraic effectsLogical methods in computer science just published Matija Pretnar's latest take on algebraic effects and handlers:
Pretnar and Bauer's Eff has made previous appearances here on LtU. Apart from the new fangled polymorphic effect system, this paper also contains an Eff tutorial. By Ohad Kammar at 2014-09-27 23:16 | Functional | Implementation | Paradigms | Semantics | Theory | 8 comments | other blogs | 10128 reads
## Breaking the Complexity Barrier of Pure Functional Programs with Impure Data StructuresBreaking the Complexity Barrier of Pure Functional Programs with Impure Data Structures by Pieter Wuille and Tom Schrijvers:
This paper is along the same lines a question I asked a couple of years ago. The idea here is to allow programming using immutable interfaces, and then automatically transform it into a more efficient mutable equivalent. |
## Browse archives## Active forum topics |

## Recent comments

9 hours 37 min ago

14 hours 28 min ago

14 hours 32 min ago

22 hours 34 min ago

1 day 2 hours ago

1 day 2 hours ago

1 day 6 hours ago

1 day 7 hours ago

1 day 7 hours ago

1 day 11 hours ago