1,720,988 research outputs found
A Syntactic Account of Singleton Types via Hereditary Substitution
No full textWe give a syntactic proof of decidability and consistency
of equivalence for the singleton type calculus, which lies at
the foundation of modern module systems such as that of
ML. Unlike existing proofs, which work by constructing a
model, our syntactic proof makes few demands on the underlying
proof theory and mathematical foundation. Consequently,
it can be | and has been | entirely formulated
in the Twelf meta-logic, and provides an important piece of
a Twelf-formalized type-safety proof for Standard ML.
The proof works by translation of the singleton type calculus
into a canonical presentation, adapted from work on
logical frameworks, in which equivalent terms are written
identically. Canonical forms are not preserved under standard
substitution, so we employ an alternative definition of
substitution called hereditary substitution, which contracts
redices that arise during substitution
Toward a Foundational Typed Assembly Language
No full textWe present the design of a typed assembly language called TALT that supports heterogeneous
tuples, disjoint sums, arrays, and a general account of addressing modes. TALT also implements
the von Neumann model in which programs are stored in memory, and supports relative addressing.
Type safety for execution and for garbage collection are shown by machine-checkable proofs. TALT
is the first formalized typed assembly language to provide any of these features
Sound and Complete Elimination of Singleton Kinds
No full textSingleton kinds provide an elegant device for expressing type equality information resulting from modern module languages, but they can complicate the metatheory of languages in which they appear. I present a translation from a language with singleton kinds to one without, and prove this translation to be sound and complete. This translation is useful for type-preserving compilers generating typed target languages. The proof of soundness and completeness is done by normalizing type equivalence derivations using Stone and Harper's type equivalence decision procedure
Higher-order Representation of Substructural Logics
No full textWe present a technique for higher-order representation of
substructural logics such as linear or modal logic. We show
that such logics can be encoded in the (ordinary) Logical
Framework, without any linear or modal extensions. Using
this encoding, metatheoretic proofs about such logics can
easily be developed in the Twelf proof assistant
Explicit Contexts in LF (Revised)
No full textThe standard methodology for representing deductive systems in LF identifies the object's language's context with the LF context. Consequently, any variable dealt with explicitly by any judgement or metatheorem must be last in the context. When the object language is dependently typed, this can pose a problem for establishing some metatheoretic results, since dependent hypotheses cannot be re-ordered at will.
This paper presents a general technique that addresses such problems, based on representing the object language's context as an explicit object in LF while retaining the use of higher-order representation for the object language's syntax. A central result is that it is possible to convert between explicit and implicit contexts, which makes it feasible to use the standard methodology for most developments, but use explicit contexts where necessary. We do not propose any extensions to LF; the technique can be utilized in standard LF
A Simple Proof of Call-by-Value Standardization
No full textWe give a simple proof of the Standardization Theorem for
call-by-value based on Takahashi's method of parallel reduction.
The proof is formalized in Twelf
Toward a Practical Type Theory for Recursive Modules
No full textModule systems for languages with complex type systems, such as Standard ML, often lack the
ability to express mutually recursive type and function dependencies across module boundaries.
Previous work by Crary, Harper and Puri [5] set out a type-theoretic foundation for recursive
modules in the context of a phase-distinction calculus for higher-order modules. Two constructs
were introduced for encoding recursive modules: a fixed-point module and a recursively dependent
signature. Unfortunately, the implementations of both constructs involve the use of equi-recursive
type constructors at higher-order kinds, the equivalence of which is not known to be decidable.
In this paper, we show that the practicality of recursive modules is not contingent upon that
of equi-recursive constructors. We begin with the theoretical infrastructure described above and
study precisely how equi-recursiveness is used in the recursive module constructs, resulting in
a clarification and generalization of the underlying ideas. We then examine in depth how the
recursive module constructs in the revised type system can serve as the target of elaboration for a
recursive module extension to Standard ML
Foundational certified code in a metalogical framework
No full textAbstract: "Foundational certified code systems seek to prove untrusted programs to be safe relative to safety policies given in terms of actual machine architectures, thereby improving the systems' flexibility and extensibility. Previous efforts have employed a structure wherein the proofs are expressed in the same logic used to express the safety policy. We propose an alternative structure wherein safety proofs are expressed in the Twelf metalogic, thereby eliminating from those proofs an extra layer of encoding needed in the previous accounts. Using this metalogical approach, we have constructed a complete, foundational account of safety for a fully expressive typed assembly language.
How to Believe a Twelf Proof
No full textLogical systems are represented in LF by giving a full and faithful (adequate)
embedding of the deductive apparatus of the logic as canonical forms of certain
types and kinds in LF in specified contexts. The collection of contexts over which
the representation is adequate is called a world, because it provides generators
for the canonical forms in question. Transferring adequacy from one world to
another relies on the concept of subordination, which expresses the irrelevance
of any “extra” variables in the target world
Syntactic Logical Relations for Polymorphic and Recursive Types
No full textThe method of logical relations assigns a relational interpretation to types that expresses operational invariants
satisfied by all terms of a type. The method is widely used in the study of typed languages, for
example to establish contextual equivalences of terms. The chief difficulty in using logical relations is to
establish the existence of a suitable relational interpretation. We extend work of Pitts and Birkedal and
Harper on constructing relational interpretations of types to polymorphism and recursive types, and apply
it to establish parametricity and representation independence properties in a purely operational setting.
We argue that, once the existence of a relational interpretation has been established, it is straightforward
to use it to establish properties of interest
- …
