the proceedings contain 7 papers. the topics discussed include: type design patterns for computer mathematics;singleton: a general-purpose dependently-typed assembly language;a type and effect system for deadlock avoi...
ISBN:
(纸本)9781450304849
the proceedings contain 7 papers. the topics discussed include: type design patterns for computer mathematics;singleton: a general-purpose dependently-typed assembly language;a type and effect system for deadlock avoidance in low-level languages;extended alias type system using separating implication;type safety from the ground up;AuraConf: a unified approach to authorization and confidentiality;information flow enforcement in monadic libraries;and the essence of monotonic state.
the proceedings contain 8 papers. the topics discussed include: towards concurrent type theory;exact type parameterization and this type support;types for relaxed memory models;towards a formal semantics for a structu...
ISBN:
(纸本)9781450311205
the proceedings contain 8 papers. the topics discussed include: towards concurrent type theory;exact type parameterization and this type support;types for relaxed memory models;towards a formal semantics for a structurally dynamic noncausal modelling language;semantics for graphical user interfaces;giving Haskell a promotion;static lock capabilities for deadlock freedom;type systems for dummies;and row-based effect types for database integration.
We present the design of a formal low-level multi-threaded language with advanced region-based memory management and synchronization primitives, where well-typed programs are memory safe and race free. In our language...
详细信息
ISBN:
(纸本)9781605588919
We present the design of a formal low-level multi-threaded language with advanced region-based memory management and synchronization primitives, where well-typed programs are memory safe and race free. In our language, regions and locks are combined in a single hierarchy and are subject to uniform ownership constraints imposed by a hierarchical structure: deallocating a region causes its sub-regions to be deallocated. Similarly, when a region is protected, then its sub-regions are also protected. We discuss aspects of the integration and implementation of the formal language within Cyclone and evaluate the performance of code produced by the modified Cyclone compiler against highly optimized C programs using atomic operations, pthreads, and OpenMP. Although our implementation is still in a preliminary stage, our results show that the performance overhead for guaranteed race freedom and memory safety is acceptable.
In the GADT (Generalized Algebraic Data types) type system, a pattern-matching branch can draw type information from boththe scrutinee type and the data constructor type. Even though the type system can handle comple...
详细信息
ISBN:
(纸本)9781605588919
In the GADT (Generalized Algebraic Data types) type system, a pattern-matching branch can draw type information from boththe scrutinee type and the data constructor type. Even though the type system can handle complex interactions between the two types, most programs require only simple interactions in the form of parametric instantiation and type indexing. To explore the tradeoffs related to GADT patterns, we define the Pointwise GADT type system, which restricts GADTs to the common case of parametric instantiation and type indexing. the Pointwise GADT type system still accepts a wide range of GADT programs, while rejecting a pathological function whose pattern-matching branches can make arbitrarily different assumptions about the type environment. We also state and prove several properties of the type system, which we speculate might be useful in helping researchers design better type inference algorithms.
Over the last 15 years, we have experienced a programming language renaissance. Numerous scripting languages have become widely used in industrial and open-source projects. they have supplemented the existing mainstre...
详细信息
ISBN:
(纸本)9781605588919
Over the last 15 years, we have experienced a programming language renaissance. Numerous scripting languages have become widely used in industrial and open-source projects. they have supplemented the existing mainstream languages-C++ and Java and, in contexts such as systems administration and web programming, they have started to play a dominant role. While each scripting language comes with its own philosophy, their designers share an antipathy to types. As a result, these languages come without a static type system. Most script developers initially welcome this freedom, but soon discover that the lack of a type system deprives them of an essential maintenance tool. My keynote explains my team's approach to equip such languages with a type system. the goal of our work is to empower programmers so that they can gradually enrich scripts withtypes on a module-by-module basis as they perform maintenance work on the system. Naturally, we wish to ensure type soundness so that the type annotations are meaningful, and we wish to accommodate the programming idioms of the original language in order to keep the overhead of type enrichment low.
We present System F degrees, an extension of System F degrees that uses kinds to distinguish between linear and unrestricted types, simplifying the use of linearity for general-purpose programming. We demonstrate thro...
详细信息
ISBN:
(纸本)9781605588919
We present System F degrees, an extension of System F degrees that uses kinds to distinguish between linear and unrestricted types, simplifying the use of linearity for general-purpose programming. We demonstrate through examples how System F degrees can elegantly express many useful protocols, and we prove that any protocol representable as a DFA can be encoded as an F type. We supply mechanized proofs of System F degrees's soundness and parametricity properties, along with a nonstandard operational semantics that formalizes common intuitions about linearity and aids in reasoning about protocols. We compare System F degrees to other linear systems, noting that the simplicity of our kind-based approach leads to a more explicit account of what linearity is meant to capture, allowing otherwise-conflicting interpretations of linearity (in particular, restrictions on aliasing versus restrictions on resource usage) to coexist peacefully. We also discuss extensions to System F degrees aimed at making the core language more practical, including the additive fragment of linear logic, algebraic datatypes, and recursion.
ML modules are a powerful language mechanism for decomposing programs into reusable components. Unfortunately, they also have a reputation for being "complex" and requiring fancy type theory that is mostly o...
详细信息
ISBN:
(纸本)9781605588919
ML modules are a powerful language mechanism for decomposing programs into reusable components. Unfortunately, they also have a reputation for being "complex" and requiring fancy type theory that is mostly opaque to non-experts. While this reputation is certainly understandable, given the many non-standard methodologies that have been developed in the process of studying modules, we aim here to demonstrate that it is undeserved. To do so, we give a very simple elaboration semantics for a full-featured, higher-order ML-like module language. Our elaboration defines the meaning of module expressions by a straightforward, compositional translation into vanilla System F-omega (the higher-order polymorphic lambda-calculus), under plain F-omega typing environments. We thereby show that ML modules are merely a particular mode of use of System F-omega. Our module language supports the usual second-class modules with Standard ML-style generative functors and local module definitions. To demonstrate the versatility of our approach, we further extend the language withthe ability to package modules as first-class values a very simple extension, as it turns out. Our approach also scales to handle OCaml-style applicative functor semantics, but the details are significantly more subtle, so we leave their presentation to a future, expanded version of this paper. Lastly, we report on our experience using the "locally nameless" approach in order to mechanize the soundness of our elaboration semantics in Coq.
In this paper we present Singleton, a dependently typed assembly language. Based upon the calculus of inductive constructions, Singleton's type system allows procedures abstracting over terms, types, propositions,...
详细信息
We develop a Haskell library for functional-logic programming, motivated by the implementation of Wired, a relational embedded domain-specific language for describing and analysing digital circuits at the VLSI-layout ...
详细信息
ISBN:
(纸本)9781595936745
We develop a Haskell library for functional-logic programming, motivated by the implementation of Wired, a relational embedded domain-specific language for describing and analysing digital circuits at the VLSI-layout level. Compared to a previous library for logic programming by Claessen and Ljunglof, we support residuation, easier creation of logical data types, and pattern matching. We discuss other applications of our library, including test-data generation, and various extensions, including lazy narrowing.
暂无评论