Building language towers with Ziggurat

2008 ◽  
Vol 18 (5-6) ◽  
pp. 707-780 ◽  
Author(s):  
DAVID FISHER ◽  
OLIN SHIVERS
Keyword(s):  
Assembly Language ◽  
Flow Analysis ◽  
Type System ◽  
Type Systems ◽  
Higher Order ◽  
Language System ◽  
Static Semantics ◽  
Language Level ◽  
Concrete Syntax ◽  
Polymorphic Type

AbstractZiggurat is a meta-language system that permits programmers to develop Scheme-like macros for languages with nontrivial static semantics, such as C or Java (suitably encoded in an S-expression concrete syntax). Ziggurat permits language designers to construct ‘towers’ of language levels with macros; each level in the tower may have its own static semantics, such as type systems or flow analyses. Crucially, the static semantics of the languages at two adjacent levels in the tower can be connected, allowing improved reasoning power at a higher level to be reflected down to the static semantics of the language level below. We demonstrate the utility of the Ziggurat framework by implementing higher level language facilities as macros on top of an assembly language, utilizing static semantics such as termination analysis, a polymorphic type system and higher order flow analysis.

A system of constructor classes: overloading and implicit higher-order polymorphism

1995 ◽  
Vol 5 (1) ◽  
pp. 1-35 ◽  
Author(s):  
Mark P. Jones
Keyword(s):  
Type System ◽  
Type Systems ◽  
Natural Generalization ◽  
Higher Order ◽  
Functional Language ◽  
Effective Algorithm ◽  
Prototype Implementation ◽  
Type Classes

AbstractThis paper describes a flexible type system that combines overloading and higher-order polymorphism in an implicitly typed language using a system of constructor classes—a natural generalization of type classes in Haskell. We present a range of examples to demonstrate the usefulness of such a system. In particular, we show how constructor classes can be used to support the use of monads in a functional language. The underlying type system permits higher-order polymorphism but retains many of the attractive features that have made Hindley/Milner type systems so popular. In particular, there is an effective algorithm that can be used to calculate principal types without the need for explicit type or kind annotations. A prototype implementation has been developed providing, amongst other things, the first concrete implementation of monad comprehensions known to us at the time of writing.

Weak polymorphism can be sound

1996 ◽  
Vol 6 (1) ◽  
pp. 111-141 ◽  
Author(s):  
John Greiner
Keyword(s):  
New Jersey ◽  
Type System ◽  
Type Systems ◽  
Type Inference ◽  
Inference Algorithm ◽  
Standard Ml ◽  
Polymorphic Type

AbstractThe weak polymorphic type system of Standard ML of New Jersey (SML/NJ) (MacQueen, 1992) has only been presented as part of the implementation of the SML/NJ compiler, not as a formal type system. As a result, it is not well understood. And while numerous versions of the implementation have been shown unsound, the concept has not been proved sound or unsound. We present an explanation of weak polymorphism and show that a formalization of this is sound. We also relate this to the SML/NJ implementation of weak polymorphism through a series of type systems that incorporate elements of the SML/NJ type inference algorithm.

scholarly journals Featherweight generic confinement

2006 ◽  
Vol 16 (6) ◽  
pp. 793-811 ◽  
Author(s):  
ALEX POTANIN ◽  
JAMES NOBLE ◽  
DAVE CLARKE ◽  
ROBERT BIDDLE
Keyword(s):  
Programming Languages ◽  
Ad Hoc ◽  
Type System ◽  
Type Systems ◽  
General Purpose ◽  
Ownership Type ◽  
Essential Change ◽  
Polymorphic Type ◽  
Syntactic Restrictions

Existing approaches to object encapsulation either rely on ad hoc syntactic restrictions or require the use of specialised type systems. Syntactic restrictions are difficult to scale and to prove correct, while specialised type systems require extensive changes to programming languages. We demonstrate that confinement can be enforced cheaply in Featherweight Generic Java, with no essential change to the underlying language or type system. This result demonstrates that polymorphic type parameters can simultaneously act as ownership parameters and should facilitate the adoption of confinement and ownership type systems in general-purpose programming languages.

scholarly journals Typing first-class continuations in ML

1993 ◽  
Vol 3 (4) ◽  
pp. 465-484 ◽  
Author(s):  
Robert Harper ◽  
Bruce F. Duba ◽  
David Macqueen
Keyword(s):  
Operational Semantics ◽  
Type System ◽  
Type Systems ◽  
Functional Language ◽  
Type Assignment ◽  
Polymorphic Type ◽  
Alternative Type

AbstractAn extension of ML with continuation primitives similar to those found in Scheme is considered. A number of alternative type systems are discussed, and several programming examples are given. A continuation-based operational semantics is defined for a small, purely functional language, and the soundness of the Damas–Milner polymorphic type assignment system with respect to this semantics is proved. The full Damas–Milner type system is shown to be unsound in the presence of first-class continuations. Restrictions on polymorphism similar to those introduced in connection with reference types are shown to suffice for soundness.

scholarly journals Reachability types: tracking aliasing and separation in higher-order functional programs

2021 ◽  
Vol 5 (OOPSLA) ◽  
pp. 1-32
Author(s):  
Yuyan Bao ◽  
Guannan Wei ◽  
Oliver Bračevac ◽  
Yuxuan Jiang ◽  
Qiyang He ◽  
...  
Keyword(s):  
Functional Programming ◽  
Type System ◽  
Type Systems ◽  
Higher Order ◽  
Ownership Type ◽  
Ownership Transfer ◽  
Reachability Sets ◽  
Programming Patterns ◽  
New Type ◽  
Higher Order Functions

Ownership type systems, based on the idea of enforcing unique access paths, have been primarily focused on objects and top-level classes. However, existing models do not as readily reflect the finer aspects of nested lexical scopes, capturing, or escaping closures in higher-order functional programming patterns, which are increasingly adopted even in mainstream object-oriented languages. We present a new type system, λ * , which enables expressive ownership-style reasoning across higher-order functions. It tracks sharing and separation through reachability sets, and layers additional mechanisms for selectively enforcing uniqueness on top of it. Based on reachability sets, we extend the type system with an expressive flow-sensitive effect system, which enables flavors of move semantics and ownership transfer. In addition, we present several case studies and extensions, including applications to capabilities for algebraic effects, one-shot continuations, and safe parallelization.

scholarly journals Automating Proof Steps of Progress Proofs: Comparing Vampire and Dafny

10.29007/5zjp ◽  
2018 ◽  
Author(s):  
Sylvia Grewe ◽  
Sebastian Erdweg ◽  
Mira Mezini
Keyword(s):  
Formal Methods ◽  
Programming Language ◽  
Type System ◽  
Type Systems ◽  
Domain Specific Languages ◽  
Smt Solver ◽  
Domain Specific ◽  
Efficient Type

\noindent Developing provably sound type systems is a non-trivial task which, as of today, typically requires expert skills in formal methods and a considerable amount of time. Our Veritas~\cite{GreweErdwegWittmannMezini15} project aims at providing support for the development of soundness proofs of type systems and efficient type checker implementations from specifications of type systems. To this end, we investigate how to best automate typical steps within type soundness proofs.\noindent In this paper, we focus on progress proofs for type systems of domain-specific languages. As a running example for such a type system, we model a subset SQL and augment it with a type system. We compare two different approaches for automating proof steps of the progress proofs for this type system against each other: firstly, our own tool Veritas, which translates proof goals and specifications automatically to TPTP~\cite{Sutcliffe98} and calls Vampire~\cite{KovacsV13} on them, and secondly, the programming language Dafny~\cite{Leino2010}, which translates proof goals and specifications to the intermediate verification language Boogie 2~\cite{Leino2008} and calls the SMT solver Z3~\cite{DeMoura2008} on them. We find that Vampire and Dafny are equally well-suited for automatically proving simple steps within progress proofs.

FIRST-CLASS CONTEXTS IN ML

2000 ◽  
Vol 11 (01) ◽  
pp. 65-87
Author(s):  
MASATOMO HASHIMOTO
Keyword(s):  
Programming Language ◽  
Operational Semantics ◽  
Type System ◽  
Type Inference ◽  
Inference Algorithm ◽  
Hole Filling ◽  
Dynamic Binding ◽  
Polymorphic Type ◽  
Open Program ◽  
Program Modules

This paper develops an ML-style programming language with first-class contexts i.e. expressions with holes. The crucial operation for contexts is hole-filling. Filling a hole with an expression has the effect of dynamic binding or macro expansion which provides the advanced feature of manipulating open program fragments. Such mechanisms are useful in many systems including distributed/mobile programming and program modules. If we can treat a context as a first-class citizen in a programming language, then we can manipulate open program fragments in a flexible and seamless manner. A possibility of such a programming language was shown by the theory of simply typed context calculus developed by Hashimoto and Ohori. This paper extends the simply typed system of the context calculus to an ML-style polymorphic type system, and gives an operational semantics and a sound and complete type inference algorithm.

Sign in / Sign up

Export Citation Format

Share Document