I present Reticulated Python, a lightweight system for experimenting with gradual-typed dialects of Python.
The dialects are syntactically identical to Python 3 but give static and dynamic?semantics to the type annotations
already present in Python 3. Reticulated Python consists of a typechecker, a source-to-source translator that inserts casts,
and Python libraries that implement the?casts. Using Reticulated Python, we study a gradual type system that features
structurally-typed objects and type inference for local variables. We evaluate two dynamic semantics for casts: one?based
on Siek and Taha (2007) and a new design, using transient casts, that does not require proxy objects. We
evaluate these designs with two third-party Python programs: the CherryPy web?framework and a library of
statistical functions.
Manifest contract calculi are a family of statically typed
higher-order contract calculi where contract information occurs as
refinement types---e.g., {x:Int|0 < x} means positive integers.
Contracts in such calculi are checked statically if possible;
otherwise dynamically with type conversion, also called casts. It
is a natural idea to apply refinement types to algebraic datatypes
because data structures are often constructed or manipulated in such
a way as to meet certain specifications---e.g., a list constructed
by a sorting function must be sorted. A naive combination, however,
leads to inefficient dynamic contract checking.
We propose *manifest datatypes*, of which argument types of data
constructors can be refined, with the mechanism of casts between
different but compatible datatypes to make dynamic contract checking
more efficient. We formalize a contract calculus for manifest
datatypes with a semantics and a type system and prove type
soundness. We also describe systematic generation of manifest
datatype definitions from refinement types, delayed contract
checking, and a prototype implementation using Camlp4.
Effect systems have the potential to help software developers, but their
? practical adoption as part of language definitions has been very limited.
? We conjecture that this??is due in part to the difficulty of transitioning from a system
? where effects are implicit and unrestricted to a system with a static effect
? discipline, which must settle for conservative checking in order to be
? decidable. ?To address this, we develop a theory of gradual effect
? checking, which makes it possible to incrementally annotate and statically
? check effects, while still rejecting statically effect-inconsistent programs. ?We
? extend the generic type-and-effect framework of Marino and Millstein with a
? notion of unknown effects, which turns out to be significantly more subtle
? than unknown types in traditional gradual typing.
This is joint work with Felipe Bañados Schwerter and Éric Tanter
Dynamically-typed OO languages have become a main staple of the practical
programmer's toolkit. Once they build large systems in these languages,
however, they realize that they want to equip their code with reliable
type information for use in maintenance, documentation, and other software
engineering tasks. While researchers have started to design gradual type systems
to support these efforts, existing systems do not yet support the most
dynamic features of these languages.
In this talk, I present an OO extension of Typed Racket. Like most dynamically
typed OO languages, Racket takes classes seriously and supports them as first-class
run-time values. As a result, Racket programmers rely on idioms such as mixins
that require first-class classes. My talk will explain how Typed Racket's
expanded type system accommodates these idioms and how its type-to-contract
compiler ensures the soundness of the boundaries between typed and untyped
components.
Joint work with: Daniel Feltey, Sam Tobin-Hochstadt, Matthias Felleisen
We address the problem of modelling and verifying
contract-oriented systems, wherein distributed agents may advertise and
stipulate contracts, but ? differently from most other approaches to
distributed agents ? are not assumed to always behave “honestly”. We model
such systems in CO2, a basic calculus for contract-oriented computing. CO2
features primitives for advertising contracts, for reaching agreements,
and for querying the fulfilment of contracts. Coordination among
participants happens via multi-party sessions, which are created once
agreements are reached.
The possibility of not keeping promises gives rise to a rich variety of
possible misbehaviours, which we illustrate with the help some examples.
We discuss some verification techniques to ensure “honesty”, namely that a
participant always respects her contracts, in all possible execution
contexts. The honesty property is quite strong, because it requires that a
participant is capable of fulfilling her obligations also when the context
plays against her. We discuss some work in progress about weaker notions
of honesty (which however still guarantee safe interactions among agents),
and their relation with different cases of inter-session dependencies. Our
final goal is a theory for blame shifting, allowing to determine when a
(not-strictly-honest) agent can blame other (dishonest) agents for her
contractual violations.
We present a theory of contracts, interpreted as multi-player
concurrent games among competitive participants. The two key notions of
our model are that of agreement and protection. The agreement property is
a game-theoretic generalization of the notion of compliance typically
studied in session behaviours: a participant agrees on a contract if she
has a strategy to reach her goals (or make another participant chargeable
for a violation), whatever the moves of her adversaries. The protection
property is relevant when contract brokers are untrusted: a participant is
protected by a contract when she has a strategy to defend herself in all
possible contexts, even in those where she has not reached an agreement.
We show that, in a relevant class of contracts, agreements and protection
mutually exclude each other. We then propose a novel formalism for
modelling contractual obligations (event structures with circular
causality), which allows us to construct contracts which guarantee both
agreements and protection. Finally, we establish a correspondence between
game-theoretic contracts and Propositional Contract Logic, by showing that
winning strategies in game-theoretic contracts are related to proofs in
the logic.
program monitoring techniques in the context of software-defined networks. ?In a software-defined network (SDN), a general-purpose controller machine decides on a global network policy and then transmits commands to many routers to implement that policy. ?A monitor for the SDN controller can sit in between the controller and the switches, monitoring the rules emitted from the controller and ensuring they establish some invariant (eg: no forwarding loops in the network; certain access control or reachability properties; etc).
Behavioral software contracts are a widely used mechanism for governing
the flow of values between components. However, run-time monitoring and
enforcement of contracts imposes significant overhead and delays
discovery of faulty components to run-time.
In this work, we tackle the problem of soft contract verification, which
aims to statically prove either complete or partial contract correctness
of components, written in an untyped, higher-order language with
first-class contracts. Our approach uses higher-order symbolic execution
that leverages contracts as a rich source of symbolic values, including
unknown behavioral values, and employs an updatable heap of contract
invariants to reason about flow-sensitive facts. The approach is able to
analyze first-class contracts, recursive data structures, unknown
functions, and control-flow-sensitive reasoning about values, which are
all idiomatic in dynamic languages. It makes effective use of an
off-the-shelf solver to decide problems without heavy encodings. The
approach is competitive with a wide range of existing tools---including
type systems, flow analyzers, and model checkers---on their own benchmarks.
Typed Racket has always relied heavily on Racket's
underlying contract system to maintain soundness when interacting with
untyped programs. But as Typed Racket has grown more sophisticated,
this has placed greater demands on the contract system. In this talk,
I'll discuss several ways in which we've approached this question, and
focus on one challenge in particular: interacting with encapsulated
and mutable state. Our solution, called chaperones, enables Typed
Racket to soundly exchange mutable data while not violating other
invariants that the system relies on.
Session types enable fine-grained static control over communication
protocols. Gradual typing is a means
to safely integrate statically and dynamically-typed program fragments.
We propose a calculus for synchronous functional two-party session
types, augment this calculus with a dynamically-typed fragment as
well as coercion operations between statically and dynamically-typed
parts, and establish its basic metatheory: type preservation and progress.
We explore two different representations for coerced communication
channels, with eager and lazy cast semantics. The lazy version is
more efficient, but requires coercion simplification to establish the
metatheory.
