## User login## Navigation |
## Theory## 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 | 13943 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 | 19742 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 | 17734 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 | 18668 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 | 2 comments | other blogs | 12246 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 | 13386 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. ## 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 | 8385 reads
## Propositions as TypesPropositions as Types, Philip Wadler. Draft, March 2014.
Philip Wadler has written a very enjoyable ( By Manuel J. Simoni at 2014-03-07 16:38 | Fun | History | Theory | 34 comments | other blogs | 21863 reads
## The marriage of bisimulations and Kripke logical relations
CK Hur, D Dreyer, G Neis, V Vafeiadis (POPL 2012). The marriage of bisimulations and Kripke logical relations.
There has been great progress in recent years on developing effective techniques for reasoning about program equivalence in ML-like languages---that is, languages that combine features like higher-order functions, recursive types, abstract types, and general mutable references. Two of the most prominent types of techniques to have emerged areI understand the paper as offering an extension to bisimulation that handles the notion of hidden transitions properly and so allows a generalisation of KLRs to any systems that can be treated using bisimulations. Applications to verified compilation are mentioned, and everything has been validated in Coq. |
## Browse archives## Active forum topics |

## Recent comments

1 week 5 days ago

2 weeks 5 days ago

5 weeks 12 hours ago

5 weeks 5 days ago

5 weeks 5 days ago

6 weeks 1 day ago

6 weeks 1 day ago

6 weeks 2 days ago

6 weeks 2 days ago

6 weeks 3 days ago