Fully Abstract Compilation via Universal Embedding by Max S. New, William J. Bowman, and Amal Ahmed:
A fully abstract compiler guarantees that two source components are observationally equivalent in the source language if and only if their translations are observationally equivalent in the target. Full abstraction implies the translation is secure: targetlanguage attackers can make no more observations of a compiled component than a sourcelanguage attacker interacting with the original source component. Proving full abstraction for realistic compilers is challenging because realistic target languages contain features (such as control effects) unavailable in the source, while proofs of full abstraction require showing that every target context to which a compiled component may be linked can be backtranslated to a behaviorally equivalent source context.
We prove the first full abstraction result for a translation whose target language contains exceptions, but the source does not. Our translation—specifically, closure conversion of simply typed λcalculus with recursive types—uses types at the target level to ensure that a compiled component is never linked with attackers that have more distinguishing power than sourcelevel attackers. We present a new backtranslation technique based on a deep embedding of the target language into the source language at a dynamic type. Then boundaries are inserted that mediate terms between the untyped embedding and the stronglytyped source. This technique allows backtranslating nonterminating programs, target features that are untypeable in the source, and wellbracketed effects.
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.
As many of you know, the email functionality of the website has not been working for a very, very long time. In addition, all new users are still being approved by me, to combat spam. All this means manual work by me, prompted by frustrated emails by new members. Alas, given other commitments, I find that the backlog is growing and I simply cannot find the time to handle these emails (i.e., approve the user, set an initial password, let them know and ask them to change it). If any member want to help me with this, I would be grateful. This will involve getting extra admin privileges on the site, after which I can forward the requests in the pipe line to you to approve.
Thanks!
Dynamic Witnesses for Static Type Errors (or, illtyped programs usually go wrong) by Eric L. Seidel, Ranjit Jhala, Westley Weimer:
Static type errors are a common stumbling block for newcomers to typed functional languages. We present a dynamic approach to explaining type errors by generating counterexample witness inputs that illustrate how an illtyped program goes wrong. First, given an illtyped function, we symbolically execute the body to dynamically synthesize witness values that can make the program go wrong. We prove that our procedure synthesizes general witnesses in that if a witness is found, then for all inhabited input types, there exist values that can make the function go wrong. Second, we show how to extend the above procedure to produce a reduction graph that can be used to interactively visualize and debug witness executions. Third, we evaluate our approach on two data sets comprising over 4,500 illtyped student programs. Our technique is able to generate witnesses for 88% of the programs, and our reduction graph yields small counterexamples for 81% of the witnesses.
Sounds like a great idea to make type systems more accessible, particularly for beginners. The current limitations are described the discussion, section 54:
There are, of course, drawbacks to our approach. Four that stand out are: (1) coverage limits due to random generation, (2) the inability to handle certain instances of infinite types, (3) dealing with an explosion in the size of generated traces, and (4) handling adhoc polymorphism.
It's also not clear whether this would produce proper witnesses for violations of higher kinded types or other more sophisticated uses of type systems. There are plenty of examples where invariants are encoded in types, eg. lightweight static capabilities.
SetTheoretic Types for Polymorphic Variants by Giuseppe Castagna, Tommaso Petrucciani, and Kim Nguyễn:
Polymorphic variants are a useful feature of the OCaml language whose current definition and implementation rely on kinding constraints to simulate a subtyping relation via unification. This yields an awkward formalization and results in a type system whose behaviour is in some cases unintuitive and/or unduly restrictive.
In this work, we present an alternative formalization of polymorphic variants, based on settheoretic types and subtyping, that yields a cleaner and more streamlined system. Our formalization is more expressive than the current one (it types more programs while preserving type safety), it can internalize some metatheoretic properties, and it removes some pathological cases of the current implementation resulting in a more intuitive and, thus, predictable type system. More generally, this work shows how to add fullfledged union types to functional languages of the ML family that usually rely on the HindleyMilner type system. As an aside, our system also improves the theory of semantic subtyping, notably by proving completeness for the type reconstruction algorithm.
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 nondeterministic (see section 5.3.2).
How to Build Static Checking Systems Using Orders of Magnitude Less Code, by Fraser Brown Andres Notzli Dawson Engler:
Modern static bug finding tools are complex. They typically consist of hundreds of thousands of lines of code, and most of them are wedded to one language (or even one compiler). This complexity makes the systems hard to understand, hard to debug, and hard to retarget to new languages, thereby dramatically limiting their scope.
This paper reduces the complexity of the checking system by addressing a fundamental assumption, the assumption that checkers must depend on a fullblown language specification and compiler front end. Instead, our program checkers are based on drastically incomplete language grammars (“microgrammars”) that describe only portions of a language relevant to a checker. As a result, our implementation is tiny—roughly 2500 lines of code, about two orders of magnitude smaller than a typical system. We hope that this dramatic increase in simplicity will allow developers to use more checkers on more systems in more languages.
We implement our approach in µchex, a languageagnostic framework for writing static bug checkers. We use it to build microgrammar based checkers for six languages (C, the C preprocessor, C++, Java, JavaScript, and Dart) and find over 700 errors in realworld projects.
Looks like an interesting approach with some compelling results, and will make a good tool for the toolbox. See also the Reddit thread for further discussion.
No value restriction is needed for algebraic effects and handlers, by Ohad Kammar and Matija Pretnar:
We present a straightforward, sound HindleyMilner polymorphic type system for algebraic effects and handlers in a callbyvalue calculus, which allows type variable generalisation of arbitrary computations, not just values. This result is surprising. On the one hand, the soundness of unrestricted callbyvalue HindleyMilner polymorphism is known to fail in the presence of computational effects such as reference cells and continuations. On the other hand, many programming examples can be recast to use effect handlers instead of these effects. Analysing the expressive power of effect handlers with respect to state effects, we claim handlers cannot express reference cells, and show they can simulate dynamically scoped state.
Looks like a nice integration of algebraic effects with simple HindlyMilner, 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.
Making signals unnecessary with The Elm Architecture
...the big benefit is that Elm is now significantly easier to learn and use. As the design of subscriptions emerged, we saw that all the toughest concepts in Elm (signals, addresses, and ports) could collapse into simpler concepts in this new world. Elm is designed for easeofuse, so I was delighted to stumble upon a path that would take us farther with fewer concepts. To put this in more alarmist terms, everything related to signals has been replaced with something simpler and nicer.
Simon Peyton Jones has been elected as a Fellow of the Royal Society. The Royal Society biography reads:
Simon's main research interest is in functional programming languages, their implementation, and their application. He was a key contributor to the design of the nowstandard functional language Haskell, and is the lead designer of the widelyused Glasgow Haskell Compiler (GHC). He has written two textbooks about the implementation of functional languages.
More generally, Simon is interested in language design, rich type systems, compiler technology, code generation, runtime systems, virtual machines, and garbage collection. He is particularly motivated by direct use of principled theory to practical language design and implementation  that is one reason he loves functional programming so much.
Simon is also chair of Computing at School, the grassroots organisation that was at the epicentre of the 2014 reform of the English computing curriculum.
Congratulations SPJ!
Kent Dybvig (Cadence Research, Cisco Systems) has released the commercial scheme compiler Chez Scheme (scheme.com) as open source on GitHub. Chez Scheme is a native code generating optimizing compiler for R6RS focusing on performance and productivity. It supports crosscompilation, threading, and many other extensions. Current version is 9.4.
I'm excited to see what the community will build with this great tool.
https://github.com/cisco/chezscheme
The paper: An ArrayOriented Language with Static Rank Polymorphism, Justin Slepak, Olin Shivers, and Panagiotis Manolios, Northeastern University, 2014.
Abstract.
The arraycomputational model pioneered by Iverson’s lan
guages APL and J offers a simple and expressive solution to the “von
Neumann bottleneck.” It includes a form of rank, or dimensional, poly
morphism, which renders much of a program’s control structure im
plicit by lifting base operators to higherdimensional array structures.
We present the first formal semantics for this model, along with the first
static type system that captures the full power of the core language.
The formal dynamic semantics of our core language, Remora, illu
minates several of the murkier corners of the model. This allows us to
resolve some of the model’s
ad hoc
elements in more general, regular
ways. Among these, we can generalise the model from SIMD to MIMD
computations, by extending the semantics to permit functions to be lifted
to higherdimensional arrays in the same way as their arguments.
Our static semantics, a dependent type system of carefully restricted
power, is capable of describing array computations whose dimensions
cannot be determined statically. The typechecking problem is decidable
and the type system is accompanied by the usual soundness theorems.
Our type system’s principal contribution is that it serves to extract the
implicit control structure that provides so much of the language’s expres
sive power, making this structure explicitly apparent at compile time.

Recent comments
10 hours 1 min ago
10 hours 58 min ago
1 day 10 hours ago
1 day 11 hours ago
3 days 19 hours ago
4 days 12 min ago
4 days 8 hours ago
4 days 17 hours ago
5 days 42 min ago
5 days 19 hours ago