Tags

spl's library 443 articles 

 

Smartest Recompilation

  [CiTO]
In Proceedings of the 20th ACM SIGPLAN-SIGACT symposium on Principles of programming languages (1993), pp. 439-450, doi:10.1145/158511.158702
posted to compilers modularity type-inference by spl on 2012-06-01 14:30:44 **

Abstract

To separately compile a program module in traditional statically-typed languages, one has to manually write down an import interface which explicitly specifies all the external symbols referenced in the module. Whenever the definitions of these external symbols are changed, the module has to be recompiled. In this paper, we present an algorithm which can automatically infer the “minimum” import interface for any module in languages based on the Damas-Milner type discipline (e.g., ML). By “minimum”, we mean that the interface specifies ...

 

Debugging Type Errors (Full version)

  [CiTO]
(5 November 1995)
posted to algorithms ml type-errors type-inference by spl  on 2012-05-31 18:50:21 *** along with 2 people and 1 group dfisher dherman NU-PRL

Abstract

Compilers for programming languages such as Standard ML are able to find many programming errors at compile time, however the diagnostic messages from the type inference algorithm do not always clearly identify the source of type errors. We argue that an extended type definition, which assigns types to open expressions as well as closed expressions, can serve as the basis for a programming environment that helps programmers debug type errors. We present such a type definition, which is closely related to ...

 

Improving Polymorphic Type Explanations

  [CiTO]
(May 2001)

Abstract

The benefits of static parametric polymorphic type checking based on the Hindley-Milner scheme are well-known: it minimizes semantic errors while improving component generality. However, systems based on the W algorithm and its variants tend to offer poor support for understanding type checking and type errors. While this efficient algorithm is widely used in functional language implementations, it does not correspond well to how people understand the types in programs. Understanding the types in reports produced by those algorithms tends to require ...

 

On the Unification of Substitutions in Type Inference Implementation of Functional Languages

  [CiTO]
In IFL 1998 (September 1998), pp. 649-650, doi:10.1007/3-540-48515-5_9

Abstract

The response of compilers to programs with type errors can be unpredictable and confusing. In part this is because the point at which type inference fails may not be the point at which the programmer has made a mistake. This paper explores a way of making type inference algorithms fail at different locations in programs so that clearer error messages may then be produced. Critical to the operation of type inference algorithms is their use of substitutions. We will see that ...

 

Coercions in Hindley-Milner Systems

  [CiTO]
Vol. 3085 (2004), pp. 259-275, doi:10.1007/978-3-540-24849-1_17
posted to coercion let-polymorphism program-transformation by spl on 2012-03-11 15:08:23 **

Abstract

Coercive subtyping is a theory of abbreviation for dependent type theories. In this paper, we incorporate the idea of coercive subtyping into the traditional Hindley-Milner type systems in functional programming languages. This results in a typing system with coercions, an extension of the Hindley-Milner type system. A type inference algorithm is developed and shown to be sound and complete with respect to the typing system. A notion of derivational coherence is developed to deal with the problem of ambiguity and the ...

 

Coercions in a polymorphic type system

  [CiTO]
Math. Struct. in Comp. Science, Vol. 18 (2008), pp. 729-751, doi:10.1017/s0960129508006804
posted to coercion let-polymorphism program-transformation type-safety by spl on 2012-03-11 15:00:06 read

Abstract

We incorporate the idea of coercive subtyping, a theory of abbreviation for dependent type theories, into the polymorphic type system in functional programming languages. The traditional type system with let-polymorphism is extended with argument coercions and function coercions, and a corresponding type inference algorithm is presented and proved to be sound and complete. ...

 

Stream Fusion on Haskell Unicode Strings

  [CiTO]
In IFL'09, Vol. 6041 (2011), pp. 125-140, doi:10.1007/978-3-642-16478-1_8
posted to fusion haskell streams strings unicode by spl on 2012-03-07 14:32:34 **

Abstract

Prior papers have presented a fusion framework called stream fusion for removing intermediate data structures from both lists and arrays in Haskell. Stream fusion is unique in using an explicit datatype to accomplish fusion. We demonstrate how this can be exploited in the creation of a new Haskell string representation Text , which achieves better performance and data density than String . Text uses streams not only to accomplish fusion, but also as a way to abstract away from various underlying ...

 

The Role of Refactorings in API Evolution

  [CiTO]
In ICSM'05 (September 2005), pp. 389-398, doi:10.1109/icsm.2005.90
posted to refactoring software-evolution by spl  on 2012-03-07 13:53:35 ** along with 5 people and 1 group adriann dannydig khatchad misto smogit Refactoring

Abstract

Frameworks and libraries change their APIs. Migrating an application to the new API is tedious and disrupts the development process. Although some tools and ideas have been proposed to solve the evolution of APIs, most updates are done manually. To better understand the requirements for migration tools we studied the API changes of three frameworks and one library. We discovered that the changes that break existing applications are not random, but they tend to fall into particular categories. Over 80% of ...

 

Binders Unbound

  [CiTO]
In ICFP 2011 (September 2011), pp. 333-345, doi:10.1145/2034574.2034818
posted to alpha-equivalence bindings fresh-names haskell by spl on 2012-03-07 13:35:49 read

Abstract

Implementors of compilers, program refactorers, theorem provers, proof checkers, and other systems that manipulate syntax know that dealing with name binding is difficult to do well. Operations such as α-equivalence and capture-avoiding substitution seem simple, yet subtle bugs often go undetected. Furthermore, their implementations are tedious, requiring "boilerplate" code that must be updated whenever the object language definition changes. Many researchers have therefore sought to specify binding syntax declaratively, so that tools can correctly handle the details behind the scenes. This ...

 

Unification: A Multidisciplinary Survey

  [CiTO]
ACM Comput. Surveys, Vol. 21, No. 1. (March 1989), pp. 93-124, doi:10.1145/62029.62030

Abstract

The unification problem and several variants are presented. Various algorithms and data structures are discussed. Research on unification arising in several areas of computer science is surveyed; these areas include theorem proving, logic programming, and natural language processing. Sections of the paper include examples that highlight particular uses of unification and the special problems encountered. Other topics covered are resolution, higher order logic, the occur check, infinite terms, feature structures, equational theories, inheritance, parallel algorithms, generalization, lattices, and other applications of ...

 

Continuation Semantics in Typed Lambda-Calculi

  [CiTO]
Vol. 193 (1985), pp. 219-224, doi:10.1007/3-540-15648-8_17
edited by Rohit Parikh
posted to continuations lambda-calculus retract semantics type-theory by spl on 2012-02-06 18:13:44 **

Abstract

This paper reports preliminary work on the semantics of the continuation transform. Previous work on the semantics of continuations has concentrated on untyped lambda-calculi and has used primarily the mechanism of inclusive predicates. Such predicates are easy to understand on atomic values, but they become obscure on functional values. In the case of the typed lambda-calculus, we show that such predicates can be replaced by retractions. The main theorem states that the meaning of a closed term is a retraction of ...

 

A Hierarchy of Mendler style Recursion Combinators: Taming Inductive Datatypes with Negative Occurrences

  [CiTO]
In Proceedings of ICFP 2011 (2011), pp. 234-246, doi:10.1145/2034773.2034807
posted to inductive-types mendler-recursion negative-types recursion by spl on 2012-01-20 12:26:59 read

Abstract

The Mendler style catamorphism (which corresponds to weak induction) always terminates even for negative inductive datatypes. The Mendler style histomorphism (which corresponds to strong induction) is known to terminate for positive inductive datatypes. To our knowledge, the literature is silent on its termination properties for negative datatypes. In this paper, we prove that histomorphisms do not always termintate by showing a counter-example. We also enrich the Mendler collection of recursion combinators by defining a new form of Mendler style catamorphism (msfcata), ...

 

Inductive types and type constraints in the second-order lambda calculus

  [CiTO]
Annals of Pure and Applied Logic, Vol. 51, No. 1-2. (14 March 1991), pp. 159-172, doi:10.1016/0168-0072(91)90069-x

Abstract

We add to the second-order lambda calculus the type constructors μ and ν, which give the least and greatest solutions to positively defined type expressions. Strong normalizability of typed terms is shown using Girard's candidat de réductibilité method. Using the same structure built for that proof, we prove a necessary and sufficient condition for determining when a collection of equational type constraints admit the typing of only strongly normalizable terms. ...

 

Introduction to Functional Programming Using Gofer

  [CiTO]
(April 1994)
posted to gofer introduction by spl on 2012-01-03 13:09:28 *
 

Towards Getting Generic Programming Ready for Prime Time

  [CiTO]
(May 2009)
 

Type-Safe Evolution of Spreadsheets Fundamental Approaches to Software Engineering

  [CiTO]
Vol. 6603 (2011), pp. 186-201, doi:10.1007/978-3-642-19811-3_14
posted to datatype-generic software-evolution spreadsheets type-safety by spl on 2011-10-07 14:05:54 **

Abstract

Spreadsheets are notoriously error-prone. To help avoid the introduction of errors when changing spreadsheets, models that capture the structure and interdependencies of spreadsheets at a conceptual level have been proposed. Thus, spreadsheet evolution can be made safe within the confines of a model. As in any other model/instance setting, evolution may not only require changes at the instance level but also at the model level. When model changes are required, the safety of instance evolution can not be guarded by the ...

 

Dynamic Language Embedding with Homogeneous Tool Support

  [CiTO]
(October 2010)
posted to domain-specific-languages editors grammars metaprogramming thesis by spl on 2011-08-22 14:01:47 **

Abstract

Domain-specific languages (DSLs) are increasingly used as embedded languages within general-purpose host languages. DSLs provide a compact,dedicated syntax for specifying parts of an application related to specialized domains. Unfortunately, such language extensions typically do not integrate well with existing development tools. Editors, compilers and debuggers are either unaware of the extensions, or must be adapted at a non-trivial cost. Furthermore, these embedded languages typically conflict with the grammar of the host language and make it difficult to write hybrid code; few ...

 

A Theory of Typed Coercions and its Applications

  [CiTO]
In ICFP 2009 (August 2009), pp. 329-340, doi:10.1145/1631687.1596598

Abstract

A number of important program rewriting scenarios can be recast as type-directed coercion insertion. These range from more theoretical applications such as coercive subtyping and supporting overloading in type theories, to more practical applications such as integrating static and dynamically typed code using gradual typing, and inlining code to enforce security policies such as access control and provenance tracking. In this paper we give a general theory of type-directed coercion insertion. We specifically explore the inherent tradeoff between expressiveness and ambiguity--the ...

 

Lightweight Monadic Programming in ML

  [CiTO]
In ICFP 2011 (September 2011)
posted to lightweight ml monads rewriting type-inference by spl on 2011-08-22 13:39:20 **

Abstract

Many useful programming constructions can be expressed as monads. Examples include probabilistic modeling, functional reactive programming, parsing, and information flow tracking, not to mention effectful functionality like state and I/O. In this paper, we present a type-based rewriting algorithm to make programming with arbitrary monads as easy as using ML's built-in support for state and I/O. Developers write programs using monadic values of type M t as if they were of type t, and our algorithm inserts the necessary binds, units, ...

 

The Semantics of Miranda's Algebraic Types

  [CiTO]
In Mathematical Foundations of Programming Language Semantics, Vol. 298 (1988), pp. 455-473, doi:10.1007/3-540-19020-1_25

Abstract

Miranda has two interesting features in its typing system: implicit polymorphism (also known as ML-style polymorphism) and algebraic types. Algebraic types create new types from old and can operate on arbitrary types. This paper argues that functions on types, or type constructors, best represent the meaning of algebraic types. Building upon this idea, we develop a denotational semantics for algebraic types. We first define a typed lambda calculus that specifies type constructors. A semantic model of type constructors is then built, ...

Note (first note only)

This is the first description of viewing algebraic datatypes as type constructors and performing kind checking.

 

A Generalized Let-Polymorphic Type Inference Algorithm

  [CiTO]
ROPAS MEMO, Vol. 2000-5 (31 March 2000)

Abstract

We present a generalized let-polymorphic type inference algorithm, prove that any of its instances is sound and complete with respect to the Hindley/Milner let-polymorphic type system, and find a condition on two instance algorithms so that one algorithm should find type errors earlier than the other. By instantiating the generalized algorithm with different parameters, we can achieve not only the two opposite algorithms (the bottom-up standard Algorithm W and the top-down folklore algorithm M) but also other various hybrid algorithms that ...

 

Top Quality Type Error Messages

  [CiTO]
(September 2005)

Abstract

Flaws in computer software are a fact of life, both in small and large-scale applications. Compilers for modern programming languages accommodate many program analyses for finding mistakes at compile-time (statically). These analyses detect a significant portion of errors automatically: this makes program analyses a valuable and indispensable tool for developing reliable, high quality software. Type checking is perhaps the most popular and best studied form of static analysis. This analysis guarantees that functions (or methods) are never applied to incompatible arguments, ...

 

Context-Sensitive Computations in Functional and Functional Logic Programs

  [CiTO]
Journal of Functional and Logic Programming, Vol. 1998, No. 1. (January 1998)

Abstract

Context-sensitive rewriting is a refined form of rewriting that explores a smaller reduction space by imposing some fixed restrictions on the replacements. Any Term Rewriting System (TRS) can be given a context-sensitive rewrite relation. In this paper, we review the theory of context-sensitive rewriting and formulate conditions to guarantee the confluence of this relation. Also, for left-linear TRSs, we show that the (eventually obtained) computed value of a given expression can also be produced by context-sensitive rewriting, thus furnishing more efficient ...

 

Systeemarchitectuur

  [CiTO]
(November 2005)
 

Design and implementation of a simple typed language based on the lambda-calculus

  [CiTO]
(May 1985)

Abstract

Despite the work of Landin and others as long ago as 1966, almost all recent programming languages are large and difficult to understand. This thesis is a re-examination of the possibility of designing and implementing a small but practical language based on very few primitive constructs. The text records the syntax and informal semantics of a new language called Ponder. The most notable features of the work are a powerful type-system and an efficient implementation of normal order reduction. In contrast to Landin’s ...

 

Category theory: a programming language-oriented introduction

  [CiTO]
(19 October 2008)
 

CiTO, the Citation Typing Ontology

  [CiTO]
Journal of Biomedical Semantics, Vol. 1, No. Suppl 1. (2010), S6, doi:10.1186/2041-1480-1-s1-s6
posted to bibliography citations ontologies owl by spl  on 2010-10-29 12:34:37 ** along with 20 people and 4 groups dartar Demeter devabhaktunisrikrishna dswan dullhunk egonw ekrzepka fairybasslet fergus gthorisson hilmerfaik jasonzou lmichan lyss mfenner mstone RafG rossmounce ruvido Scis0000002 Biiiogeek frao_lab Gobbledygook Journal picks

Abstract

CiTO, the Citation Typing Ontology, is an ontology for describing the nature of reference citations in scientific research articles and other scholarly works, both to other such publications and also to Web information resources, and for publishing these descriptions on the Semantic Web. Citation are described in terms of the factual and rhetorical relationships between citing publication and cited publication, the in-text and global citation frequencies of each cited work, and the nature of the cited work itself, including its publication ...

 

An Introduction to Knuth-Bendix Completion

  [CiTO]
The Computer Journal, Vol. 34, No. 1. (1 January 1991), pp. 2-15, doi:10.1093/comjnl/34.1.2
posted to algorithms completion equational-reasoning proofs rewriting strategies by spl  on 2010-10-29 12:25:31 ** along with 2 people JavaJoe radico

Abstract

An informal introduction is given to the underlying concepts of term rewriting. Topics covered are Knuth-Bendix completion, completion modulo equations, unfailing completion and theorem proving by completion. ...

 

Une extension de l'interprétation de Gödel à l'analyse, et son application à l'élimination de coupures dans l'analyse et la théorie des types

  [CiTO]
In Proceedings of the 2nd Scandinavian Logic Symposium (1971), pp. 63-92
edited by J. E. Fenstad
posted to system-f type-checking type-theory by spl on 2010-10-22 14:10:22 ** along with 1 person samth
 

An ML Editor Based on Proofs-as-Programs

  [CiTO]
Automated Software Engineering, International Conference on, Vol. 0 (1999), 166, doi:10.1109/ase.1999.802196
posted to curry-howard-isomorphism editors ml proofs termination type-safety by spl on 2010-09-10 16:28:07 **

Abstract

CYNTHIA is a novel editor for the functional programming language ML in which each function definition is represented as the proof of a simple specification. Users of \cynthia edit programs by applying sequences of high-level editing commands to existing programs. These commands make changes to the proof representation from which a new program is then extracted. The use of proofs is a sound framework for analyzing ML programs and giving useful feedback about errors. Amongst the properties analyzed within CYNTHIA at ...

 

Structure and Interpretation of Computer Programs

  [CiTO]
(25 July 1996)
posted to abstraction book compilers computer-science data-structures interpreters metaprogramming modularity mutability program-structure register-machines by spl  on 2010-07-12 13:54:34 ** along with 26 people adamnellis awils1 azazello brady calvins chaoxu dullhunk higepon jasmithoffice josezarza karthikraman KnayaWP msaeli myspl newdawn nicholasVaidyanathan NickGasson olegus robertlischke robotact srccheck timflutre tnhh triampurum trm005 vlasovskikh

Abstract

Abelson and Sussman's classic <I>Structure and Interpretation of Computer Programs</I> teaches readers how to program by employing the tools of abstraction and modularity. The authors' central philosophy is that programming is the task of breaking large problems into small ones. The book spends a great deal of time considering both this decomposition and the process of knitting the smaller pieces back together.<P> The authors employ this philosophy in their writing technique. The text asks the broad question "What is programming?" Having ...

 

Structured Programming

  [CiTO]
(1972)
posted to book data-structures hierarchical-structure program-design program-structure proofs sequence stepwise-composition by spl  on 2010-07-12 13:26:02 ** along with 5 people gvdh michaelbanks oanam rafaelsiza tnhh

Abstract

In recent years there has been an increasing interest in the art of computer programming, the conceptual tools available for the design of programs, and the prevention of programming oversights and error. The initial outstanding contribution to our understanding of this subject was made by E. W. Dijkstra, whose Notes on Structured Programming form the first and major section of this book. They clearly expound the reflections of a brilliant programmer on the methods which he has hitherto unconsciously applied; there ...

 

Generic Point-free Lenses

  [CiTO]
In Mathematics of Program Construction , Vol. 6120 (2010), pp. 331-352, doi:10.1007/978-3-642-13321-3_19

Abstract

Lenses are one the most popular approaches to define bidirectional transformations between data models. A bidirectional transformation with view-update, denoted a lens, encompasses the definition of a forward transformation projecting concrete models into abstract views, together with a backward transformation instructing how to translate an abstract view to an update over concrete models. In this paper we show that most of the standard point-free combinators can be lifted to lenses with suitable backward semantics, allowing us to use the point-free style ...

 

Arity-generic datatype-generic programming

  [CiTO]
In PLPV '10: Proceedings of the 4th ACM SIGPLAN workshop on Programming languages meets program verification (2010), pp. 15-26, doi:10.1145/1707790.1707799

Abstract

Some programs are doubly-generic. For example, map is datatype-generic in that many different data structures support a mapping operation. A generic programming language like Generic Haskell can use a single definition to generate map for each type. However, map is also arity-generic because it belongs to a family of related operations that differ in the number of arguments. For lists, this family includes repeat, map, zipWith, zipWith3, zipWith4, etc. With dependent types or clever programming, one can unify all of these ...

 

A poor man's concurrency monad

  [CiTO]
Journal of Functional Programming, Vol. 9, No. 03. (May 1999), pp. 313-323, doi:10.1017/s0956796899003342
posted to concurrency haskell monads by spl  on 2010-07-05 12:48:21 ** along with 6 people and 2 groups dalev draganigajic janschaefer jcreed keigoi pedagand NU-PRL TU-KL-SoftwareTechnologyGroup

Abstract

Without adding any primitives to the language, we define a concurrency monad transformer in Haskell. This allows us to add a limited form of concurrency to any existing monad. The atomic actions of the new monad are lifted actions of the underlying monad. Some extra operations, such as fork, to initiate new processes, are provided. We discuss the implementation, and use some examples to illustrate the usefulness of this construction. ...

 

Term Rewriting and All That

  [CiTO]
In Term Rewriting and All That (1998)
 

Web programming in Haskell

  [CiTO]
(23 April 2010)

Abstract

In this thesis we show how to do web programming in the statically typed Haskell programming language, applying programming language research to the web programming world. We construct three libraries that encompass a framework for building database-driven web applications. ...

 

A Compact Fixpoint Semantics for Term Rewriting Systems

  [CiTO]
Theoretical Computer Science (24 May 2010), doi:10.1016/j.tcs.2010.05.012

Abstract

This work is motivated by the fact that a “compact” semantics for term rewriting systems, which is essential for the development of effective semantics-based program manipulation tools (e.g. automatic program analyzers and debuggers), does not exist. The big-step rewriting semantics that is most commonly considered in functional programming is the set of values/normal forms that the program is able to compute for any input expression. Such a big-step semantics is unnecessarily oversized, as it contains many “semantically useless” elements that can be ...

 

Functional Pearl: Scrap Your Zippers

  [CiTO]
(16 June 2007)
posted to gadts generics haskell zipper by spl on 2010-05-19 16:25:33 read along with 1 person robertjohnsimmons

Abstract

The "zipper" data type provides the ability for editing tree shaped data in a pure functional setting and has found many uses and applications. However the traditional zipper has two major limitations. First, requires a significant amount of boilerplate code to implement. Second, it can only operate on homogeneous data types. Data structures where there are multiple node types are beyond the range of what it can handle. The generic zipper developed in this paper solves both these issues while maintaining type ...

 

Type Specialisation for the λ-calculus; or, A New Paradigm for Partial Evaluation Based on Type Inference

  [CiTO]
In Partial Evaluation (1996), pp. 183-215, doi:10.1007/3-540-61580-6_10
 

A Theory of Typed Hygienic Macros

  [CiTO]
(May 2010)

Abstract

We present the λm-calculus, a semantics for a language of hygienic macros with a non-trivial theory. Unlike Scheme, where programs must be macro-expanded to be analyzed, our semantics admits reasoning about programs as they appear to programmers. Our contributions include a semantics of hygienic macro expansion, a formal definition of α-equivalence that is independent of expansion, and a proof that expansion preserves α-equivalence. The key technical component of our language is a type system similar to Culpepper and Felleisen’s “shape types,” ...

 

Ott: Effective tool support for the working semanticist

  [CiTO]
Journal of Functional Programming, Vol. 20, No. 01. (2010), pp. 71-122, doi:10.1017/s0956796809990293

Abstract

Semantic definitions of full-scale programming languages are rarely given, despite the many potential benefits. Partly this is because the available metalanguages for expressing semantics – usually either for informal mathematics or the formal mathematics of a proof assistant – make it much harder than necessary to work with large definitions. We present a metalanguage specifically designed for this problem, and a tool, Ott, that sanity-checks such definitions and compiles them into proof assistant code for Coq, HOL, and Isabelle/HOL, together ...

 

Ott: Effective Tool Support for the Working Semanticist

  [CiTO]
In ICFP 2007 (2007), pp. 1-12, doi:10.1145/1291151.1291155
posted to formalization ott programming-language proofs semantics theorem-proving verification by spl  on 2010-05-07 12:32:02 ** along with 6 people and 1 group jakobro marcinzalewski pedagand robertjohnsimmons StevenKeuchel sweirich ConcertRG

Abstract

It is rare to give a semantic definition of a full-scale programming language, despite the many potential benefits. Partly this is because the available metalanguages for expressing semantics - usually either LaTeX for informal mathematics, or the formal mathematics of a proof assistant - make it much harder than necessary to work with large definitions.We present a metalanguage specifically designed for this problem, and a tool, ott, that sanity-checks such definitions and compiles them into proof assistant code for Coq, HOL, ...

 

Generic Programs and Proofs

  [CiTO]
(2000)
 

Deforestation: Transforming programs to eliminate trees

  [CiTO]
Theoretical Computer Science, Vol. 73, No. 2. (June 1990), pp. 231-248, doi:10.1016/0304-3975(90)90147-a

Abstract

An algorithm that transforms programs to eliminate intermediate trees is presented. The algorithm applies to any term containing only functions with definitions in a given syntactic form, and is suitable for incorporation in an optimizing compiler. ...

 

VMKit: a Substrate for Managed Runtime Environments

  [CiTO]
SIGPLAN Not. In VEE '10: Proceedings of the 6th ACM SIGPLAN/SIGOPS international conference on Virtual execution environments, Vol. 45 (March 2010), pp. 51-62, doi:10.1145/1735997.1736006

Abstract

Managed Runtime Environments (MREs), such as the JVM and the CLI, form an attractive environment for program execution, by providing portability and safety, via the use of a bytecode language and automatic memory management, as well as good performance, via just-in-time (JIT) compilation. Nevertheless, developing a fully featured MRE, including e.g. a garbage collector and JIT compiler, is a herculean task. As a result, new languages cannot easily take advantage of the benefits of MREs, and it is difficult to experiment ...

 

The Future of Programming

  [CiTO]
Commun. ACM, Vol. 25, No. 3. (1982), pp. 196-206, doi:10.1145/358453.358459
posted to programming-environment software-engineering by spl on 2010-04-26 08:41:40 **

Abstract

The nature of programming is changing. These changes will accelerate as improved software development practices and more sophisticated development tools and environments are produced. This paper surveys the most likely changes in the programming task and in the nature of software over the short term, the medium term, and the long term. In the short term, the focus is on gains in programmer productivity through improved tools and integrated development environments. In the medium term, programmers will be able ...

 

The Study of Programming Languages

  [CiTO]
(01 July 1994)
 

Type-driven Defunctionalization

  [CiTO]
In ICFP '97, Vol. 32, No. 8. (August 1997), pp. 25-37, doi:10.1145/258948.258953

Abstract

In 1972, Reynolds outlined a general method for eliminating functional arguments known as defunctionalization . The idea underlying defunctionalization is encoding a functional value as first-order data, and then realizing the applications of the encoded function via an apply function. Although this process is simple enough, problems arise when defunctionalization is used in a polymorphic language. In such a language, a functional argument of a higher-order function can take different type instances in different applications. As a consequence, ...

 

A Categorical Unification Algorithm

  [CiTO]
In Category Theory and Computer Programming (1986), pp. 493-505, doi:10.1007/3-540-17162-2_139
posted to algorithms category-theory ml unification by spl on 2010-04-08 17:33:24 **

Abstract

This is a case study in the design of computer programs based upon the twin themes of abstraction and constructivity. We consider the unification of terms--a symbol-manipulative task widely used in computation--and derive a unification algorithm based upon constructions in category theory. This hinges on two observations. Firstly, unification may be considered as an instance of something more abstract--as a colimit in a suitable category. Secondly, general constructions of colimits provide recursive procedures for computing the unification of terms. We have ...

Note: You may cite this page as: http://www.citeulike.org/user/spl

Result page: 1 2 3 4 5 6 7 8 9 Next

Create CiTO

Create a CiTO relationship by dragging the [CiTO] link onto another article.

Alternatively, drag two articles into the two boxes below. This is useful when the two articles are not on the same page - the articles will be remembered between pages.

This article...

...this one

Privacy Statement | Terms & Conditions
CiteULike organises scholarly (or academic) papers or literature and provides bibliographic (which means it makes bibliographies) for universities and higher education establishments. It helps undergraduates and postgraduates. People studying for PhDs or in postdoctoral (postdoc) positions. The service is similar in scope to EndNote or RefWorks or any other reference manager like BibTeX, but it is a social bookmarking service for scientists and humanities researchers.