Skip to main content
Fachgebiete
Automobil + Motoren Bauwesen + Immobilien Business IT + Informatik Elektrotechnik + Elektronik Energie + Nachhaltigkeit Finance + Banking Management + Führung Marketing + Vertrieb Maschinenbau + Werkstoffe Versicherung + Risiko
DE
EN
Bücher
Zeitschriften
Themenseiten
Organisationspsychologie Projektmanagement Marketing Smart Manufacturing
Weitere Formate
Podcasts Webinare Technik Webinare Wirtschaft Kongresse Veranstaltungskalender Awards
Jetzt Einzelzugang starten
Zugang für Unternehmen
Referenzkunden
SLX-Digitalkonferenz: Zukunftswerkstatt 2024

Mehr Umsatz mit Top-Kontakten

Am 7. Mai erfahren Sie, wie Vertriebsteams Leadgenerierung, Leadnurturing und Leadstrategien effizient steuern können.
Erweiterte Suche
Anmelden
nach oben

2009 | Buch

Well-Typed Programs Can’t Be Blamed Kapitel lesen Erstes Kapitel lesen

Programming Languages and Systems

18th European Symposium on Programming, ESOP 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings

herausgegeben von: Giuseppe Castagna

Verlag: Springer Berlin Heidelberg

Buchreihe : Lecture Notes in Computer Science

Enthalten in: Springer Professional "Wirtschaft+Technik" , Springer Professional "Technik" , Springer Professional "Wirtschaft"

Einloggen, um Zugang zu erhalten
insite
SUCHEN

Über dieses Buch

This book constitutes the refereed proceedings of the 18th European Symposium on Programming, ESOP 2009, held in York, UK, in March 2009, as part of ETAPS 2009, the European Joint Conferences on Theory and Practice of Software. The 26 revised full papers presented together with two abstracts of invited talks were carefully reviewed and selected from 98 full paper submissions. The topics addressed are typed functional programming, computational effects, types for object-oriented languages, verification, security, concurrency, service-oriented computing, parallel and concurrent programming.

Inhaltsverzeichnis

Frontmatter

Typed Functional Programming

Well-Typed Programs Can’t Be Blamed
Abstract
We introduce the blame calculus, which adds the notion of blame from Findler and Felleisen’s contracts to a system similar to Siek and Taha’s gradual types and Flanagan’s hybrid types. We characterise where positive and negative blame can arise by decomposing the usual notion of subtype into positive and negative subtypes, and show that these recombine to yield naive subtypes. Naive subtypes previously appeared in type systems that are unsound, but we believe this is the first time naive subtypes play a role in establishing type soundness.
Philip Wadler, Robert Bruce Findler
Exploring the Design Space of Higher-Order Casts
Abstract
This paper explores the surprisingly rich design space for the simply typed lambda calculus with casts and a dynamic type. Such a calculus is the target intermediate language of the gradually typed lambda calculus but it is also interesting in its own right. In light of diverse requirements for casts, we develop a modular semantic framework, based on Henglein’s Coercion Calculus, that instantiates a number of space-efficient, blame-tracking calculi, varying in what errors they detect and how they assign blame. Several of the resulting calculi extend work from the literature with either blame tracking or space efficiency, and in doing so reveal previously unknown connections. Furthermore, we introduce a new strategy for assigning blame under which casts that respect traditional subtyping are statically guaranteed to never fail. One particularly appealing outcome of this work is a novel cast calculus that is well-suited to gradual typing.
Jeremy Siek, Ronald Garcia, Walid Taha
Practical Variable-Arity Polymorphism
Abstract
Just as some functions have uniform behavior over distinct types, other functions have uniform behavior over distinct arities. These variable-arity functions are widely used in scripting languages such as Scheme and Python. Statically typed languages also accommodate modest forms of variable-arity functions, but even ML and Haskell, languages with highly expressive type systems, cannot type check the wide variety of variable-arity functions found in untyped functional languages. Consequently, their standard libraries contain numerous copies of the same function definition with slightly different names.
As part of the Typed Scheme project—an on-going effort to create an explicitly typed sister language for PLT Scheme—we have designed and implemented an expressive type system for variable-arity functions. Our practical validation in the context of our extensive code base confirms the usefulness of the enriched type system.
T. Stephen Strickland, Sam Tobin-Hochstadt, Matthias Felleisen
Resolving Inductive Definitions with Binders in Higher-Order Typed Functional Programming
Abstract
This paper studies inductive definitions involving binders, in which aliasing between free and bound names is permitted. Such aliasing occurs in informal specifications of operational semantics, but is excluded by the common representation of binding as meta-level λ-abstraction. Drawing upon ideas from functional logic programming, we represent such definitions with aliasing as recursively defined functions in a higher-order typed functional programming language that extends core ML with types for name-binding, a type of “semi-decidable propositions” and existential quantification for types with decidable equality. We show that the representation is sound and complete with respect to the language’s operational semantics, which combines the use of evaluation contexts with constraint programming. We also give a new and simple proof that the associated constraint problem is NP-complete.
Matthew R. Lakin, Andrew M. Pitts

ETAPS Invited Talk

Using Category Theory to Design Programming Languages
Abstract
In a 1980 paper entitled “Using Category Theory to Design Conversions and Generic Operators”, the author showed how the concepts of category theory can guide the design of a programming language to avoid anomalies in the interaction of implicit conversions and generic operators.
John C. Reynolds

Computational Effects

Modular Monad Transformers
Abstract
During the last two decades, monads have become an indispensable tool for structuring functional programs with computational effects. In this setting, the mathematical notion of a monad is extended with operations that allow programmers to manipulate these effects. When several effects are involved, monad transformers can be used to build up the required monad one effect at a time. Although this seems to be modularity nirvana, there is a catch: in addition to the construction of a monad, the effect-manipulating operations need to be lifted to the resulting monad. The traditional approach for lifting operations is non-modular and ad-hoc. We solve this problem with a principled technique for lifting operations that makes monad transformers truly modular.
Mauro Jaskelioff
Handlers of Algebraic Effects
Abstract
We present an algebraic treatment of exception handlers and, more generally, introduce handlers for other computational effects representable by an algebraic theory. These include nondeterminism, interactive input/output, concurrency, state, time, and their combinations; in all cases the computation monad is the free-model monad of the theory. Each such handler corresponds to a model of the theory for the effects at hand. The handling construct, which applies a handler to a computation, is based on the one introduced by Benton and Kennedy, and is interpreted using the homomorphism induced by the universal property of the free model. This general construct can be used to describe previously unrelated concepts from both theory and practice.
Gordon Plotkin, Matija Pretnar

Types for Object-Oriented Languages

Is Structural Subtyping Useful? An Empirical Study
Abstract
Structural subtyping is popular in research languages, but all mainstream object-oriented languages use nominal subtyping. Since languages with structural subtyping are not in widespread use, the empirical questions of whether and how structural subtyping is useful have thus far remained unanswered. This study aims to provide answers to these questions. We identified several criteria that are indicators that nominally typed programs could benefit from structural subtyping, and performed automated and manual analyses of open-source Java programs based on these criteria. Our results suggest that these programs could indeed be improved with the addition of structural subtyping. We hope this study will provide guidance for language designers who are considering use of this subtyping discipline.
Donna Malayeri, Jonathan Aldrich
An Interval-Based Inference of Variant Parametric Types
Abstract
Variant parametric types represent the successful integration of subtype and parametric polymorphism to support a more flexible subtyping for Java like languages. A key feature that helps strengthen this integration is the use-site variance. Depending on how the fields are used, each variance denotes a covariant, a contravariant, an invariant or a bivariant subtyping. By annotating variance properties on each type argument to a parametric class, programmers can choose various desirable variance properties for each use of the parametric class. Although Java library classes have been successfully refactored to use variant parametric types, these mechanisms are often criticized, due to the difficulty of choosing appropriate variance annotations. Several algorithms have been proposed for automatically refactoring legacy Java code to use generic libraries, but none can support the full flexibility of the use-site variance-based subtyping. This paper addresses this difficulty by proposing a novel interval-based approach to inferring both the variance annotations and the type arguments. Each variant parametric type is regarded as an interval type with two type bounds, a lower bound for writing and an upper bound for reading. We propose a constraint-based inference algorithm  that works on a per method basis, as a summary-based analysis.
Florin Craciun, Wei-Ngan Chin, Guanhua He, Shengchao Qin
Existential Quantification for Variant Ownership
Abstract
Ownership types characterize the topology of objects in the heap, through a characterization of the context to which an object belongs. They have been used to support reasoning, memory management, concurrency, etc. Subtyping is traditionally invariant w.r.t. contexts, which has often proven inflexible in some situations. Recent work has introduced restricted forms of subtype variance and unknown context, but in a rather ad-hoc and restricted way.
We develop Jo∃, a calculus which supports parameterisation of types, as well as contexts, and allows variant subtyping of contexts based on existential quantification. Jo∃ is more expressive, general, and uniform than previous works which add variance to ownership languages. Our explicit use of existential types makes the connection to type-theoretic foundations from existential types more transparent. We prove type soundness for Jo∃ and extend it to Jo∃  deep which enforces the owners-as-dominators property.
Nicholas Cameron, Sophia Drossopoulou

Verification

Formalising and Verifying Reference Attribute Grammars in Coq
Abstract
Reference attribute grammars are a powerful formalism for concisely specifying and implementing static analyses. While they have proven their merit in practical applications, no attempt has so far been made to rigorously verify correctness properties of the resulting systems. We present a general method for formalising reference attribute grammars in the theorem prover Coq. The formalisation is supported by tools for generating standard definitions from an abstract description and custom proof tactics to help automate verification. As a small but typical application, we show how closure analysis for the untyped lambda calculus can easily be implemented and proved correct with respect to an operational semantics. To evaluate the feasibility of our approach on larger systems, we implement name lookup for a naming core calculus of Java and give a formal correctness proof of the centrepiece of a rename refactoring for this language.
Max Schäfer, Torbjörn Ekman, Oege de Moor
Verified, Executable Parsing
Abstract
We describe the mechanisation of an SLR parser produced by a parser generator, covering background properties of context-free languages and grammars, as well as the construction of an SLR automaton. Among the various properties proved about the parser we show, in particular, soundness: if the parser results in a parse tree on a given input, then the parse tree is valid with respect to the grammar, and the leaves of the parse tree match the input; completeness: if the input is in the language of the grammar then the parser constructs the correct parse tree for the input with respect to the grammar; and non-ambiguity: grammars successfully converted to SLR automata are unambiguous.
We also develop versions of the algorithms that are executable by automatic translation from HOL to SML. These alternative versions of the algorithms require some interesting termination proofs.
Aditi Barthwal, Michael Norrish
An Efficient Algorithm for Solving the Dyck-CFL Reachability Problem on Trees
Abstract
The context-free language (CFL) reachability problem is well known and studied in computer science, as a fundamental problem underlying many important static analyses such as points-to-analysis. Solving the CFL reachability problem in the general case is very hard. Popular solutions resorting to a graph traversal exhibit a time complexity of O(k 3 n 3) for a grammar of size k. For Dyck CFLs, a particular class of CFLs, this complexity can be reduced to O(kn 3). Only recently the first subcubic algorithm was proposed by Chaudhuri, dividing the complexity of predating solutions by a factor of logn.
In this paper we propose an effective algorithm for solving the CFL reachability problem for Dyck languages when the considered graph is a bidirected tree with specific constraints. Our solution pre-processes the graph in O(n logn logk) time in a space of O(n logn), after which any Dyck-CFL reachability query can be answered in O(1) time, while a naïve online algorithm will require O(n) time to answer a query or require O(n 2) to store the pre-computed results for all pairs of nodes.
Hao Yuan, Patrick Eugster
Amortised Memory Analysis Using the Depth of Data Structures
Abstract
Hofmann and Jost have presented a heap space analysis [1] that finds linear space bounds for many functional programs. It uses an amortised analysis: assigning hypothetical amounts of free space (called potential) to data structures in proportion to their sizes using type annotations. Constraints on these annotations in the type system ensure that the total potential assigned to the input is an upper bound on the total memory required to satisfy all allocations.
We describe a related system for bounding the stack space requirements which uses the depth of data structures, by expressing potential in terms of maxima as well as sums. This is achieved by adding extra structure to typing contexts (inspired by O’Hearn’s bunched typing [2]) to describe the form of the bounds. We will also present the extra steps that must be taken to construct a typing during the analysis.
Brian Campbell

ESOP Invited Talk

The Financial Crisis, a Lack of Contract Specification Tools: What Can Finance Learn from Programming Language Design?
Abstract
The magnitude and dramatic consequences of the current “financial crisis” are publicly well documented. Even non professionals may read in, say, newspapers about notions like “derivatives”, “over the counter deals”, “complexity of contracts”, “insufficient regulation” or “impossible to understand portfolios” while reading about bankruptcy or bailouts of big financial institutions.
Jean-Marc Eber

Security

All Secrets Great and Small
Abstract
Tools for analysing secure information flow are almost exclusively based on ideas going back to Denning’s work from the 70’s. This approach embodies an imperfect notion of security which turns a blind eye to information flows which are encoded in the termination behaviour of a program. In exchange for this weakness many more programs are deemed ”secure”, using conditions which are easy to check. Previously it was thought that such leaks are limited to at most one bit per run. Recent work by Askarov et al (ESORICS’08) offers some bad news and some good news: the bad news is that for programs which perform output, the amount of information leaked by a Denning style analysis is not bounded; the good news is that if secrets are chosen to be sufficiently large and sufficiently random then they cannot be effectively leaked at all. The problem addressed in this paper is that secrets cannot always be made sufficiently large or sufficiently random. Contrast, for example, an encryption key with an “hasHIV”-field of a patient record. In recognition of this we develop a notion of secret-sensitive noninterference in which “small” secrets are handled more carefully than “big” ones. We illustrate the idea with a type system which combines a liberal Denning-style analysis with a more restrictive system according to the nature of the secrets at hand.
Delphine Demange, David Sands
Type-Based Automated Verification of Authenticity in Cryptographic Protocols
Abstract
Gordon and Jeffrey have proposed a type and effect system for checking authenticity in cryptographic protocols. The type system reduces the protocol verification problem to the type checking problem, but protocols must be manually annotated with non-trivial types and effects. To automate the verification of cryptographic protocols, we modify Gordon and Jeffrey’s type system and develop a type inference algorithm. Key modifications for enabling automated type inference are introduction of fractional effects and replacement of typing rules with syntax-directed ones. We have implemented and tested a prototype protocol verifier based on our type system.
Daisuke Kikuchi, Naoki Kobayashi

Concurrency

A Theory of Non-monotone Memory (Or: Contexts for free)
Abstract
We develop a general method of proving contextual properties—including (but not limited to) observational equivalence, space improvement, and memory safety under arbitrary contexts—for programs in untyped call-by-value λ-calculus with first-class, higher-order references (ref, : = and !) and deallocation (free). The method significantly generalizes Sumii et al.’s environmental bisimulation technique, and gives a sound and complete characterization of each proved property, in the sense that the “bisimilarity” (the largest set satisfying the bisimulation-like conditions) equals the set of terms with the property to be proved. We give examples of contextual properties concerning typical data structures such as linked lists, binary search trees, and directed acyclic graphs with reference counts, all with deletion operations that release memory.
This shows the scalability of the environmental approach from contextual equivalence to other binary relations (such as space improvement) and unary predicates (such as memory safety), as well as to languages with non-monotone store, where Kripke-style logical relations have difficulties.
Eijiro Sumii
Abstraction for Concurrent Objects
Abstract
Concurrent data structures are usually designed to satisfy correctness conditions such as sequential consistency and linearizability. In this paper, we consider the following fundamental question: what guarantees are provided by these conditions for client programs? We formally show that these conditions can be characterized in terms of observational refinement. Our study also provides a new understanding of sequential consistency and linearizability in terms of abstraction of dependency between computation steps of client programs.
Ivana Filipović, Peter O’Hearn, Noam Rinetzky, Hongseok Yang
Minimization Algorithm for Symbolic Bisimilarity
Abstract
The operational semantics of interactive systems is usually described by labeled transition systems. Abstract semantics is defined in terms of bisimilarity that, in the finite case, can be computed via the well-known partition refinement algorithm. However, the behaviour of interactive systems is in many cases infinite and thus checking bisimilarity in this way is unfeasible. Symbolic semantics allows to define smaller, possibly finite, transition systems, by employing symbolic actions and avoiding some sources of infiniteness. Unfortunately, the standard partition refinement algorithm does not work with symbolic bisimilarity.
Filippo Bonchi, Ugo Montanari

Service-Oriented Computing

Conversation Types
Abstract
We present a type theory for analyzing concurrent multiparty interactions as found in service-oriented computing. Our theory introduces a novel and flexible type structure, able to uniformly describe both the internal and the interface behavior of systems, referred respectively as choreographies and contracts in web-services terminology. The notion of conversation builds on the fundamental concept of session, but generalizes it along directions up to now unexplored; in particular, conversation types discipline interactions in conversations while accounting for dynamical join and leave of an unanticipated number of participants. We prove that well-typed systems never violate the prescribed conversation constraints. We also present techniques to ensure progress of systems involving several interleaved conversations, a previously open problem.
Luís Caires, Hugo Torres Vieira
Abstract Processes in Orchestration Languages
Abstract
Orchestrators are descriptions at implementation level and may contain sensitive information that should be kept private. Consequently, orchestration languages come equipped with a notion of abstract processes, which enable the interaction among parties while hiding private information. An interesting question is whether an abstract process accurately describes the behavior of a concrete process so to ensure that some particular property is preserved when composing services. In this paper we focus on compliance, i.e, the correct interaction of two orchestrators and we introduce two definitions of abstraction: one in terms of traces, called trace-based abstraction, and the other as a generalization of symbolic bisimulation, called simulation-based abstraction. We show that simulation-based abstraction is strictly more refined than trace-based abstraction and that simulation-based abstraction behaves well with respect to compliance.
Maria Grazia Buscemi, Hernán Melgratti
Global Principal Typing in Partially Commutative Asynchronous Sessions
Abstract
We generalise a theory of multiparty session types for the π-calculus through asynchronous communication subtyping, which allows partial commutativity of actions with maximal flexibility and safe optimisation in message choreography. A sound and complete algorithm for the subtyping relation, which can calculate conformance of optimised end-point processes to an agreed global specification, is presented. As a complementing result, we show a type inference algorithm for deriving the principal global specification from end-point processes which is minimal with respect to subtyping. The resulting theory allows a programmer to choose between a top-down and a bottom-up style of communication programming, ensuring the same desirable properties of typable processes.
Dimitris Mostrous, Nobuko Yoshida, Kohei Honda
Tisa: A Language Design and Modular Verification Technique for Temporal Policies in Web Services
Abstract
Web services are distributed software components, that are decoupled from each other using interfaces with specified functional behaviors. However, such behavioral specifications are insufficient to demonstrate compliance with certain temporal non-functional policies. An example is demonstrating that a patient’s health-related query sent to a health care service is answered only by a doctor (and not by a secretary). Demonstrating compliance with such policies is important for satisfying governmental privacy regulations. It is often necessary to expose the internals of the web service implementation for demonstrating such compliance, which may compromise modularity. In this work, we provide a language design that enables such demonstrations, while hiding majority of the service’s source code. The key idea is to use greybox specifications to allow service providers to selectively hide and expose parts of their implementation. The overall problem of showing compliance is then reduced to two subproblems: whether the desired properties are satisfied by the service’s greybox specification, and whether this greybox specification is satisfied by the service’s implementation. We specify policies using LTL and solve the first problem by model checking. We solve the second problem by refinement techniques.
Hridesh Rajan, Jia Tao, Steve Shaner, Gary T. Leavens

Parallel and Concurrent Programming

Automatic Parallelization with Separation Logic
Abstract
Separation logic is a recent approach to the analysis of pointer programs in which resource separation is expressed with a logical connective in assertions that describe the state at any given point in the program. We extend this approach to express properties of memory separation between different points in the program, and present an algorithm for determining independences between program statements which can be used for parallelization.
Mohammad Raza, Cristiano Calcagno, Philippa Gardner
Deny-Guarantee Reasoning
Abstract
Rely-guarantee is a well-established approach to reasoning about concurrent programs that use parallel composition. However, parallel composition is not how concurrency is structured in real systems. Instead, threads are started by ‘fork’ and collected with ‘join’ commands. This style of concurrency cannot be reasoned about using rely-guarantee, as the life-time of a thread can be scoped dynamically. With parallel composition the scope is static.
In this paper, we introduce deny-guarantee reasoning, a reformulation of rely-guarantee that enables reasoning about dynamically scoped concurrency. We build on ideas from separation logic to allow interference to be dynamically split and recombined, in a similar way that separation logic splits and joins heaps. To allow this splitting, we use deny and guarantee permissions: a deny permission specifies that the environment cannot do an action, and guarantee permission allow us to do an action. We illustrate the use of our proof system with examples, and show that it can encode all the original rely-guarantee proofs. We also present the semantics and soundness of the deny-guarantee method.
Mike Dodds, Xinyu Feng, Matthew Parkinson, Viktor Vafeiadis
A Basis for Verifying Multi-threaded Programs
Abstract
Advanced multi-threaded programs apply concurrency concepts in sophisticated ways. For instance, they use fine-grained locking to increase parallelism and change locking orders dynamically when data structures are being reorganized. This paper presents a sound and modular verification methodology that can handle advanced concurrency patterns in multi-threaded, object-based programs. The methodology is based on implicit dynamic frames and uses fractional permissions to support fine-grained locking. It supports concepts such as multi-object monitor invariants, thread-local and shared objects, thread pre- and postconditions, and deadlock prevention with a dynamically changeable locking order. The paper prescribes the generation of verification conditions in first-order logic, well-suited for scrutiny by off-the-shelf SMT solvers. A verifier for the methodology has been implemented for an experimental language, and has been used to verify several challenging examples including hand-over-hand locking for linked lists and a lock re-ordering algorithm.
K. Rustan M. Leino, Peter Müller
SingleTrack: A Dynamic Determinism Checker for Multithreaded Programs
Abstract
Multithreaded programs are prone to errors caused by unintended interference between concurrent threads. This paper focuses on verifying that deterministically-parallel code is free of such thread interference errors. Deterministically-parallel code may create and use new threads, via fork and join, and coordinate their behavior with synchronization primitives, such as barriers and semaphores. Such code does not satisfy the traditional non-interference property of atomicity (or serializability), however, and so existing atomicity tools are inadequate for checking deterministically-parallel code. We introduce a new non-interference specification for deterministically-parallel code, and we present a dynamic analysis to enforce it. We also describe SingleTrack, a prototype implementation of this analysis. SingleTrack’s performance is competitive with prior atomicity checkers, but it produces many fewer spurious warnings because it enforces a more general non-interference property that is applicable to more software.
Caitlin Sadowski, Stephen N. Freund, Cormac Flanagan
Backmatter
Metadaten
Titel
Programming Languages and Systems
herausgegeben von
Giuseppe Castagna
Copyright-Jahr
2009
Verlag
Springer Berlin Heidelberg
Electronic ISBN
978-3-642-00590-9
Print ISBN
978-3-642-00589-3
DOI
https://doi.org/10.1007/978-3-642-00590-9

Premium Partner

    Bildnachweise