We present FunTAL, the first multi-language system to formalize safe interoperability between a high-level functional language and low-level assembly code while supporting compositional reasoning about the mix. A central challenge in developing such a multi-language is how to bridge the gap between assembly, which is staged into calls to continuations, and high-level code, where subterms return a result. We present a compositional stack-based typed assembly language that supports components, comprised of one or more basic blocks, that may be embedded in high-level contexts. We also present a logical relation for FunTAL that supports reasoning about equivalence of high-level components and their assembly replacements, mixed-language programs with callbacks between languages, and assembly components comprised of different numbers of basic blocks.
We present a type checker and stepper for the FunTAL machine semantics. We include well-typed, runnable examples from the paper, as well as a few smaller examples to start with. With our artifact, you write programs and then type check / load them into a FunTAL machine. You can then step forward and backwards through the evaluation. At each step, the machine shows the registers, stack, and heap, as well as the redex and the context.
Important: the programs entered
into the editor should be Fun programs at the top; a pure
TAL component C
can be embedded as FT[t,?]C where t is
the return type, as we see in examples below. We do this so
that all programs run through the stepper have a return value.
Note: there are some syntactic differences from the presentation in the paper, which nonetheless we expect will be the primary reference for the language. These changes were made to eliminate the necessity of unicode, reduce ambiguity in the grammar, and make the type checking algorithm syntax-directed. We summarize these changes at the bottom of this page.
Examples from paper:
Additional examples: Import | Simple call | Omega | Mutable reference
Examples with errors:
| Paper | Artifact | Description |
|---|---|---|
(ι; ..., l → h, ...)
|
([instr; ...],[l -> h, ...])
|
TAL components use brackets around instructions and the heap fragment. |
τFT e
|
FT[t,s] e
|
FT (Fun outside, TAL inside) boundary
specifies the type s that the stack has after running e.
|
τFT e
|
FT[t,?] e
|
FT boundaries can use ? to indicate
that running e will not modify the type of
the stack (though values may be modified), allowing s
to be inferred.
|
import r,σTFτ e
|
import r1, s as z, t TF{e};
|
import binds the stack s on
return as z with Fun expression e of
type t.
|
α, ζ, ε
|
a1, z21, e5
|
TAL type variables must begin with a, stack
variables with z, and return marker variables
with e.
|
· | τ :: ...
|
:: | t :: ... ::
|
Empty stack prefixes (in protect, stack modifying
lambdas) are written as ::, and stack prefixes
end with ::.
|
∀, μ, λ, ∃, •
|
forall, mu, lam, exists, *
|
Greek letters and quantifiers are replaced by english keywords. |
•
|
*
|
The concrete stack symbol • is written *.
|
u[ω]
|
u[ω, ω...]
|
TAL instantiation is n-ary. (This was mentioned as syntactic sugar.) |
{χ; σ}q
|
{χ; σ} q
|
The return marker superscript is just written in line. |
λφφ(x:τ...).t
|
lam[φ][φ](x:τ...).e,(τ...) [φ] -> [φ] τ
|
The stack prefixes of stack-modifying functions are bracketed, in line. |
unpack <α, rd> u
|
unpack <α, rd>, u
|
The TAL instruction unpack has comma-separated argument,
for consistency with other instructions.
|
l -> <1, 2>,
|
[l -> ref <1, 2>,
|
Heap values are preceded by an explicit mutability marker box or ref.
|