916 papers · page 23 of 46
Abstract Several proof-assistants rely on the very formal basis of Pure Type Systems (PTS) as their foundations. We are concerned with the issues involved in the development of large proofs in these provers such as namespace management, development of reusable proof libraries and…
Abstract We bridge two distinct approaches to one-pass CPS transformations, i.e, CPS transformations that reduce administrative redexes at transformation time instead of in a post-processing phase. One approach is compositional and higher-order, and is independently due to Appel,…
Abstract Existential types provide a simple and elegant foundation for understanding generative abstract data types of the kind supported by the Standard ML module system. However, in attempting to extend ML with support for recursive modules, we have found that the traditional e…
Abstract Delimited continuations are more expressive than traditional abortive continuations and they apparently require a framework beyond traditional continuation-passing style (CPS). We show that this is not the case: standard CPS is sufficient to explain the common control op…
The Tenth ACM SIGPLAN International Conference on Functional Programming (ICFP) was held in September, 2005, in Tallinn, Estonia; Benjamin Pierce chaired the program committee. After the conference, extended versions of some of the presented papers were solicited for this special…
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 …
Abstract Monads are commonplace programming devices that are used to uniformly structure computations; in particular, they are often used to mimic the effects of impure features such as state, error handling, and I/O. This paper further develops the monadic programming paradigm b…
Abstract The LF logical framework codifies a methodology for representing deductive systems, such as programming languages and logics, within a dependently typed λ-calculus. In this methodology, the syntactic and deductive apparatus of a system is encoded as the canonical forms o…
Abstract Asynchronous exceptions, or interrupts , are important for writing robust, modular programs, but are traditionally viewed as being difficult from a semantic perspective. In this article, we present a simple, formally justified, semantics for interrupts. Our approach is t…
Abstract Haskell's popularity has driven the need for ever more expressive type system features, most of which threaten the decidability and practicality of Damas-Milner type inference. One such feature is the ability to write functions with higher-rank types – that is, functions…
This is the first textbook containing a complete, in depth description of SMIL.SMIL is an XML language, promulgated by the World Wide Web Consortium, for multimedia authoring.SMIL may be used to create sophisticated multi and hyper-media artifacts by means of the temporal and spa…
Abstract We examine the ML pattern-matching anomalies of useless clauses and non-exhaustive matches. We state the definition of these anomalies, building upon pattern matching semantics, and propose a simple algorithm to detect them. We have integrated the algorithm in the Object…
Programming" framework, Yampa.If you like little languages, you'll appreciate how useful Haskell is for embedded domain specific languages.It may be even more useful now that Template Haskell is in the works.
Abstract Let ${\cal A}$ be a set of modules and parameterized modules including type sharing constraint specifications. We prove that determining the set of the effective modules described by ${\cal A}$ is undecidable. As a consequence, type sharing constraints are proved to be n…
Abstract Design and quality are fundamental themes in engineering education. Functional programming builds software from small components, a central element of good design, and facilitates reasoning about correctness, an important aspect of quality. Software engineering courses t…
Abstract Existing languages provide good support for typeful programming of stand-alone programs. In a distributed system, however, there may be interaction between multiple instances of many distinct programs, sharing some (but not necessarily all) of their module structure, and…
Abstract Functional dependencies are a popular and useful extension to Haskell style type classes. We give a reformulation of functional dependencies in terms of Constraint Handling Rules (CHRs). In previous work, CHRs have been employed for describing user-programmable type exte…
Abstract Safety has become a fundamental requirement in all aspects of computer systems. Object-oriented calculi, such as Castagna's λ&-calculus and its variants (Castagna, 1997) ensure type safety in environments based on the distinguished object-oriented paradigm. Although for …