| |
In POPL’11: Proceedings of the 38th annual ACM SIGPLAN-SIGACT symposium on Principles of Programming Languages (2011), pp. 447-458, doi:10.1145/1926385.1926436
posted to pl substructural types
by tov
on 2011-04-06 04:50:22
Abstract
Alms is a general-purpose programming language that supports practical affine types. To offer the expressiveness of Girard’s linear logic while keeping the type system light and convenient, Alms uses expressive kinds that minimize notation while maximizing polymorphism between affine and unlimited types. A key feature of Alms is the ability to introduce abstract affine types via ML-style signature ascription. In Alms, an interface can impose stiffer resource usage restrictions than the principal usage restrictions of its implementation. This form of sealing allows ...
|
| |
Lecture Notes in Computer Science In ESOP’10: Proceedings of the 19th European Symposium on Programming, Vol. 6012 (2010), pp. 550-569, doi:10.1007/978-3-642-11957-6_29
Abstract
Affine type systems manage resources by preventing some values from being used more than once. This offers expressiveness and performance benefits, but difficulty arises in interacting with components written in a conventional language whose type system provides no way to maintain the affine type systemâs aliasing invariants. We propose and implement a technique that uses behavioral contracts to mediate between code written in an affine language and code in a conventional typed language. We formalize our approach via a typed calculus ...
|
| |
Abstract
Higher-order abstract syntax provides a convenient way of embedding domain-specific languages, but is awkward to analyse and manipulate directly. We explore the boundaries of higher-order abstract syntax. Our key tool is the unembedding of embedded terms as de Bruijn terms, enabling intensional analysis. As part of our solution we present techniques for separating the definition of an embedded program from its interpretation, giving modular extensions of the embedded language, and different ways to encode the types of the embedded language. ...
|
| |
Abstract
This paper presents a polymorphic type system for a language with delimited control operators, shift and reset. Based on the monomorphic type system by Danvy and Filinski, the proposed type system allows pure expressions to be polymorphic. Thanks to the explicit presence of answer types, our type system satisfies various important properties, including strong type soundness, existence of principal types and an inference algorithm, and strong normalization. Relationship to CPS translation as well as extensions to impredicative polymorphism are also discussed. ...
|
| |
posted to concurrency pl
by tov
on 2011-04-06 04:33:54
Abstract
How should Erlang talk to the outside world? --- this question becomes interesting if we want to build distributed applications where Erlang is one of a number of communicating components.We assume these components interact by exchanging messages --- at this level of abstraction, details of programming language, operating system and host architecture are irrelevant. What is important is the ease with which we can construct such systems, and the precision with which we can isolate faulty components in such a system. ...
|
| |
In ICFP '05: Proceedings of the tenth ACM SIGPLAN international conference on Functional programming (2005), pp. 78-91, doi:10.1145/1086365.1086376
Abstract
The concept of a "unique" object arises in many emerging programming languages such as Clean, CQual, Cyclone, TAL, and Vault. In each of these systems, unique objects make it possible to perform operations that would otherwise be prohibited (e.g., deallocating an object) or to ensure that some obligation will be met (e.g., an opened file will be closed). However, different languages provide different interpretations of "uniqueness" and have different rules regarding how unique objects interact with the rest of the language.Our ...
|
| |
In Proceedings of the 9th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (1982), pp. 207-212, doi:10.1145/582153.582176
Abstract
An abstract is not available. ...
|
| |
In In Proceedings of the 2004 ACM SIGPLAN International Conference on Functional Programming (ICFP’04 (2004), pp. 150-161
posted to pl types
by tov
on 2010-04-20 04:00:44
Abstract
We study a type system equipped with universal types and equirecursive types, which we refer to as F . We show that type equality may be decided in time O(n log n), an improvement over the previous known bound of O(n ). In fact, we show that two more general problems, namely entailment of type equations and type unification, may be decided in time O(n log n), a new result. To achieve this bound, we associate, with every ...
|
| |
posted to contexts logic pl
by tov
on 2009-10-22 18:50:23
Abstract
The Theory of Contexts is a type-theoretic axiomatization aiming to give a metalogical account of the fundamental notions of variable and context as they appear in Higher Order Abstract Syntax. In this paper, we prove that this theory is consistent by building a model based on functor categories . By means of a suitable notion of forcing , we prove that this model validates Classical Higher Order Logic, the Theory of Contexts, and also (parametrised) ...
|
| |
In OOPSLA '08: Proceedings of the 23rd ACM SIGPLAN conference on Object-oriented programming systems languages and applications (2008), pp. 227-244, doi:10.1145/1449764.1449783
Abstract
The atomic block, a synchronization primitive provided to programmers in transactional memory systems, has the potential to greatly ease the development of concurrent software. However, atomic blocks can still be used incorrectly, and race conditions can still occur at the level of application logic. In this paper, we present a intraprocedural static analysis, formalized as a type system and proven sound, that helps programmers use atomic blocks correctly. Using access permissions , which describe how objects are aliased and modified, ...
|
| |
In PLDI '02: Proceedings of the ACM SIGPLAN 2002 Conference on Programming language design and implementation, Vol. 37, No. 5. (May 2002), pp. 13-24, doi:10.1145/512529.512532
Abstract
A type system with linearity is useful for checking software protocols andresource management at compile time. Linearity provides powerful reasoning about state changes, but at the price of restrictions on aliasing. The hard division between linear and nonlinear types forces the programmer to make a trade-off between checking a protocol on an object and aliasing the object. Most onerous is the restriction that any type with a linear component must itself be linear. Because of this, checking a protocol on an ...
|
| |
In ESOP ’92: 4th European Symposium on Programming, Rennes, France, Proceedings, Vol. 582 (1992), pp. 390-407
Abstract
Linear types provide the framework for a safe embedding of mutable state in functional languages by enforcing the principle that variables of linear type must be used exactly once. A potential disadvantage of this approach is that it places read accesses to suchvariables under the same restriction as write accesses, and thus prevents reads to proceed in parallel. We present here an extension of linear types which augments the usual distinction between linear and non-linear bya ...
|
| |
posted to mine
by tov
on 2008-10-30 14:57:00
Abstract
Objective Caml is a flexible, expressive programming language, but for manipulating Unix processes, nothing beats the terseness and clarity of Bourne Shell: ls *.docx | wc -l To achieve the same effect in C requires several more lines of code and, very likely, a glance at the manual page for readdir(). Despite OCaml's excellent Unix module, which provides access to a wide variety of system calls, a task as simple as counting the .docx files in the current directory ...
|
| |
SIGPLAN Notices In Haskell '08: Proceedings of the First ACM SIGPLAN Symposium on Haskell, Vol. 44 (September 2008), pp. 25-36, doi:10.1145/1411286.1411290
Abstract
We describe an implementation of session types in Haskell. Session types statically enforce that client-server communication proceeds according to protocols. They have been added to several concurrent calculi, but few implementations of session types are available. Our embedding takes advantage of Haskell where appropriate, but we rely on no exotic features. Thus our approach translates with minimal modification to other polymorphic, typed languages such as ML and Java. Our implementation works with existing Haskell concurrency mechanisms, handles multiple communication channels and ...
|
| |
Journal of Functional Programming, Vol. 17, No. 02. (2006), pp. 145-205
posted to ml pl types
by tov
on 2008-06-04 18:28:12
Abstract
Many modern programming languages support basic generics, sufficient to implement type-safe polymorphic containers. Some languages have moved beyond this basic support, and in doing so have enabled a broader, more powerful form of generic programming. This paper reports on a comprehensive comparison of facilities for generic programming in eight programming languages: C++, Standard ML, Objective Caml, Haskell, Eiffel, Java, C# (with its proposed generics extension), and Cecil. By implementing a substantial example in each of these languages, we illustrate how the ...
|
| |
Science of Computer Programming, Vol. 37, No. 1--3. (2000), pp. 67-111
Abstract
this paper. Pleasingly, the arrow interface turned out to be applicable to other kinds of non-monadic library also, for example the fudgets library for graphical user interfaces [CH93], and a new library for programming active web pages. These applications will be described in sections 6 and 9. While arrows are a little less convenient to use than monads, they have significantly wider applicability. They can therefore be used to bring the benefits of monad-like programming to a much wider class ... ...
|
| |
posted to history icfp08 pl types
by tov
on 2008-03-30 18:21:06
Abstract
Without Abstract ...
|
| |
Theory and Practice of Object Systems, Vol. 4, No. 1. (1998), pp. 27-50
posted to icfp08 ml pl
by tov
on 2008-03-29 22:59:30
along with 1 person
Ema
Abstract
Objective ML is a small practical extension to ML with objects and top level classes. It is fully compatible with ML; its type system is based on ML polymorphism, record types with polymorphic access, and a better treatment of type abbreviations. Objective ML allows for most features of object-oriented languages including multiple inheritance, methods returning self and binary methods as well as parametric classes. This demonstrates that objects can be added to strongly typed languages based on ... ...
|
| |
|
| |
ACM SIG\-PLAN Notices, Vol. 36, No. 3. (2001), pp. 41-53
Abstract
We present a type system for a language based on F# , which allows certain type annotations to be elided in actual programs. Local type inference determines types by a combination of type propagation and local constraint solving, rather than by global constraint solving. We refine the previously existing local type inference system of Pierce and Turner[PT98] by allowing partial type information to be propagated. This is expressed by coloring types to indicate propagation directions. Propagating ... ...
|
| |
Mathematical Structures in Computer Science, Vol. 6, No. 6. (1996), pp. 579-612
Abstract
This paper is an elaborated version of the work presented in Barendsen and Smetsers (1995a) and Barendsen and Smetsers (1995c). 2. Term graph rewriting ...
|
| |
Information and Computation, Vol. 115, No. 1. (1994), pp. 38-94
Abstract
We present a new approach to proving type soundness for Hindley/Milner-style polymorphic type systems. The keys to our approach are (1) an adaptation of subject reduction theorems from combinatory logic to programming languages, and (2) the use of rewriting techniques for the specification of the language semantics. The approach easily extends from polymorphic functional languages to imperative languages that provide references, exceptions, continuations, and similar features. We illustrate the ... ...
|
| |
Abstract
In ordinary lambda calculus the occurrences of a bound variable are made recognizable by the use of one and the same (otherwise irrelevant) name at all occurrences. This convention is known to cause considerable trouble in cases of substitution. In the present paper a different notational system is developed, where occurrences of variables are indicated by integers giving the “distance” to the binding λ instead of a name attached to that λ. The system is claimed to be efficient for automatic ...
|
| |
Abstract
A new family of clipping algorithms is described. These algorithms are able to clip polygons against irregular convex plane-faced volumes in three dimensions, removing the parts of the polygon which lie outside the volume. In two dimensions the algorithms permit clipping against irregular convex windows. Polygons to be clipped are represented as an ordered sequence of vertices without repetition of first and last, in marked contrast to representation as a collection of edges as was heretofore the common procedure. ...
|
| |
In PLDI '91: Proceedings of the ACM SIGPLAN 1991 conference on Programming language design and implementation, Vol. 26, No. 6. (June 1991), pp. 293-305, doi:10.1145/113445.113470
|
| |
In PLDI '06: Proceedings of the 2006 ACM SIGPLAN conference on Programming language design and implementation (2006), pp. 295-307, doi:10.1145/1133981.1134016
|
| |
The Haskell Mailing List (12 December 2007)
posted to haskell icfp08 pl types
by tov
on 2008-03-27 11:11:29
|
| |
The Haskell Mailing List (18 December 2006)
posted to haskell icfp08 pl types
by tov
on 2008-03-27 11:10:15
|
| |
Abstract
A heterogeneous collection is a datatype that is capable of storing data of different types, while providing operations for look-up, update, iteration, and others. There are various kinds of heterogeneous collections, differing in representation, invariants, and access operations. We describe HList --- a Haskell library for strongly typed heterogeneous collections including extensible records. We illustrate HList's benefits in the context of type-safe database access in Haskell. The HList library relies on common extensions of Haskell 98. Our exploration raises interesting issues ...
|
| |
(1999)
posted to concurrency haskell icfp08 ml pl
by tov
on 2008-03-27 10:52:17
|
| |
In Conference Record of POPL '96: The $23^\text{rd}$ ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (February 1996), pp. 295-308
Abstract
Some applications are most easily expressed in a programming language that supports concurrency, notably interactive and distributed systems. We propose extensions to the purely-functional language Haskell that allows it to express explicitly concurrent applications; we call the resulting language Concurrent Haskell. The resulting system appears to be both expressive and efficient, and we give a number of examples of useful abstractions that can be built from our primitives. We have developed a ... ...
|
| |
In Proc. UK Joint Framework for Information Technology ({JFIT}) Technical Conference (93)
Abstract
We give an overview of the Glasgow Haskell compiler, focusing especially on way in which we have been able to exploit the rich theory of functional languages to give very practical improvements in the compiler. The compiler is portable, modular, generates good code, and is freely available. 1 Introduction Computer Science is both a scientific and an engineering discipline. As a scientific discipline, it seeks to establish generic principles and theories that can be used to explain or underpin a ... ...
|
| |
(05 May 2003)
Abstract
Haskell is the world's leading lazy functional programming language and is widely used in teaching, research, and applications. The language continues to develop rapidly, but in 1998 the programming community decided to capture a stable snapshot of the language by introducing Haskell 98. This book constitutes the agreed definition of Haskell 98, the language itself as well as its supporting libraries, and should be a standard reference work for anyone involved in research, teaching, or applications. All Haskell compilers support ...
|
| |
(2003)
Abstract
We define a language whose type system, incorporating session types, allows complex protocols to be specified by types and verified by static typechecking. A session type, associated with a communication channel, specifies not only the data types of individual messages, but also the state transitions of a protocol and hence the allowable sequences of messages. Although session types are well understood in the context of the #-calculus, our formulation is based on #-calculus with... ...
|
| |
In ESOP '99: Proceedings of the 8th European Symposium on Programming Languages and Systems (1999), pp. 74-90
posted to concurrency icfp08 pl types
by tov
on 2008-03-27 10:43:59
|
| |
In ESOP '88: Proceedings of the 2nd European Symposium on Programming (1988), pp. 131-144
|
| |
Proceedings of Workshop on Mathematically Structured Functional Programming In MSFP 2006 (July 2006)
Abstract
Moggi’s Computational Monads and Power et al’s equivalent notion of Freyd category have captured a large range of computational effects present in programming languages such as exceptions, side-effects, input/output and continuations. We present generalisations of both constructs, which we call parameterised monads and parameterised Freyd categories, that also capture computational effects with parameters. Examples of such are composable continuations, side-effects where the type of the state varies and input/output where the range of inputs and outputs varies. By also considering monoidal ...
|
| |
(2005)
Abstract
In this paper, we explore an extension to Haskell type classes that allows a type class declaration to define data types as well as values (or methods). Similarly, an instance declaration gives a witness for such data types, as well as a witness for each method. It turns out that this extension directly supports the idea of a type-indexed type, and is useful in many applications, especially for self-optimising libraries that adapt their data representations and algorithms in a type-directed... ...
|
| |
(2004)
Abstract
A session type is an abstraction of a set of sequences of heterogeneous values sent and received over a communication channel. Session types can be used for specifying stream-based Internet protocols. ...
|
| |
In SIGPLAN Conference on Programming Language Design and Implementation (1994), pp. 24-35
Abstract
Some algorithms make critical internal use of updatable state, even though their external specification is purely functional. Based on earlier work on monads, we present a way of securely encapsulating such stateful computations, in the context of a non-strict, purely-functional language. There are two main new developments in this paper. First, we show how to use the type system to securely encapsulate stateful computations, including ones which manipulate multiple, named, mutable objects.... ...
|
| |
Abstract
This paper explores a new point in the design space of formal reasoning systems - part programming language, part logical framework. The system is built on a programming language where the user expresses equality constraints between types and the type checker then enforces these constraints. This simple extension to the type system allows the programmer to describe properties of his program in the types of witness objects which can be thought of as concrete evidence that the program has the... ...
|
| |
In Symposium on Principles of Programming Languages (1998), pp. 289-302
Abstract
Dynamic typing extends statically typed languages with a universal datatype, simplifying programs which must manipulate other programs as data, such as distributed, persistent, interpretive and generic programs. Current approaches, however, limit the use of polymorphism in dynamic values, and can be syntactically awkward. We introduce a new approach to dynamic typing, based on staged computation, which allows a single typereconstruction algorithm to execute partly at compile time and partly at... ...
|
| |
(4 February 2005)
posted to parproj pl
by tov
on 2007-09-15 00:15:22
|
| |
posted to compilers parproj pl
by tov
on 2007-09-14 23:54:35
|
| |
In 2nd ACM SIGPLAN Workshop on Continuations (14 January 1997)
posted to parproj pl
by tov
on 2007-09-14 23:46:17
along with 1 person
steshaw
Abstract
It is well known [Wand] that concurrency can be expressed within languages that provide a continuation type. However, a number of misconceptions persist regarding the relationship between threads and continuations. I discuss the proper relationship between these two objects, and present a model for directly expressing concurrency using continuations. The model is designed to support systems programming, and has several novel features: it is synchronous, preemptable, and fully virtualisable, allowing schedulers to be written by unprivileged users that are indistinguishable from top-level schedulers that actually control access to the ...
|
| |
Abstract
An abstract is not available. ...
|
| |
posted to apl parproj pl
by tov
on 2007-09-13 22:36:06
along with 1 person
randerr
|
| |
Abstract
The importance of nomenclature, notation, and language as tools of thought has long been recognized. In chemistry and in botany, for example, the establishment of systems of nomenclature by Lavoisier and Linnaeus did much to stimulate and to channel later investigation. Concerning language, George Boole in his Laws of Thought [1, p.21] asserted "That language is an instrument of human reason, and not merely a medium for the expression of thought, is a truth generally admitted. ...
|
| |
Parallel Architecture and Compilation Techniques, 2004. PACT 2004. Proceedings. 13th International Conference on In Parallel Architecture and Compilation Techniques, 2004. PACT 2004. Proceedings. 13th International Conference on (2004), pp. 7-16
Abstract
Many advances in automatic parallelization and optimization have been achieved through the polyhedral model. It has been extensively shown that this computational model provides convenient abstractions to reason about and apply program transformations. Nevertheless, the complexity of code generation has long been a deterrent for using polyhedral representation in optimizing compilers. First, code generators have a hard time coping with generated code size and control overhead that may spoil theoretical benefits achieved by the transformations. Second, this step is usually time ...
|
| |
In SIGPLAN '86: Proceedings of the 1986 SIGPLAN symposium on Compiler construction (1986), pp. 176-185, doi:10.1145/12276.13329
posted to compilers parproj pl
by tov
on 2007-09-13 22:30:34
|
Search
