The Essence of Functional Programming
This paper explores the use monads to structure functional programs. No prior knowledge of monads or category theory is required.
2,199 papers · page 86 of 110
A Logical View of Composition and Refinement
We define two logics of safety specifications for reactive systems. The logics provide a setting for the study of composition and refinement rules, and a framework for the use of the modular specification methods that these rules underpin. The two logics arise naturally from exta…
A Relational Approach to Strictness Analysis for Higher-Order Polymorphic Functions
This paper defines the categorical notions of relators and transformations and shows that these concepts enable us to give a semantics for polymorphic, higher order functional programs.We demonstrate the pertinence of this semantics to the analysis of polymorphic programs by prov…
Static Type Inference in a Dynamically Typed Language
We present a type inference system for FL based on an operational, rather than a denotational, formulation of types. The essential elements of the system are a type language based on regular trees and a type inference logic that implements an abstract interpretation of the operat…
Subtyping Recursive Types
Article Free Access Share on Subtyping recursive types Authors: Roberto M. Amadio LIENS, Ecole Normale Supérieure, Paris LIENS, Ecole Normale Supérieure, ParisView Profile , Luca Cardelli DEC, Systems Research Center DEC, Systems Research CenterView Profile Authors Info & Claims …
"Look Ma, No Hashing, And No Arrays Neither"
It is generally assumed that hashing is essential to many algorithms related to efficient compilation; e.g., symbol table formation and maintenance, grammar manipulation, basic block optimization, and global optimization.This paper questions this assumption, and initiates develop…
Automatic Construction of Sparse Data Flow Evaluation Graphs
In this paper, we present an algorithm that con-structs sparse evaluation graphs for forward or backward monotone data flow problems. The sparse graph combines information as early as possible, yet directly connects nodes that generate and use information. This allows problems fr…
Macros That Work
Article Macros that work Share on Authors: William Clinger Department of Computer Science, University of Oregon Department of Computer Science, University of OregonView Profile , Jonathan Rees Artificial Intelligence Laboratory, Massachusetts Institute of Technology, Cambridge, M…
Static and Dynamic Semantics Processing
This paper presents a step forward in the use of partial evaluation for interpreting and compiling programs, as well as for automatically generating a compiler from denotational definitions of programming languages. We determine the static and dynamic semantics of a programming l…
Parameter-Passing and the Lambda Calculus
The choice of a parameter-passing technique is an important decision in the design of a high-level programming language. To clarify some of the semantic aspects of the decision, we develop, analyze, and compare modifications of the $\\lambda$-calculus for the most common paramete…
Typing First-Class Continuations in ML
An extension of Standard ML with continuation primitives similar to those found in Scheme is considered.A number of alternative type systems are discussed, and several programming examples are given.The semantics of type assignment for a small, purely functional fragment of the l…
A Record Calculus Based on Symmetric Concatenation
Type systems for operations on extensible records form sumpt ion; we argue that the resulting system is more straightforward than subsumption-based alternatives.
The Complexity of Type Inference for Higher-Order Typed Lambda Calculi
We analyze the computational complexity of type inference for untyped A.terms in the second-order polymorphic typed ~-calculus (l'z) invented by Gi-
Temporal Proof Methodologies for Real-time Systems
. We extend the specification language of temporal logic, the corresponding verification framework, and the underlying computational model to deal with real-time properties of concurrent and reactive systems. A global, discrete, and asynchronous clock is incorporated into the mod…
Coordinating First-Order Multiparty Interactions
A first-order multiparty interaction is an abstraction mechanism that defines communication among a set of formal process roles. Actual processes participate in a first-order interaction by enroling into roles, and execution of the interaction can proceed when all roles are fille…
Algebraic Reconstruction of Types and Effects
We present the first algorithm for reconstructing the types and effects of expressions in the presence of first class procedures in a polymorphic typed language, Effects are static descriptions of the dynamic behavior of expressions.Just as a type describes what an expression com…
Communication with Directed Logic Variables
Pointer-Induced Aliasing: A Problem Classification
A?iasing occurs at some program point during execution when two or more names exist for the same location. We have isolated various programming language mechanisms which create aliases. We have classified the complexity of the fllas problem induced by each mechanism alone and in …
Polymorphic Type Inference and Assignment
We present a new approach to the polymorphic typing of data accepting in-place modification in ML-like languages.This approach is based on restrictions over type generalization, and a refined typing of functions.The type system given here leads to a better integration of imperati…
Parallel Programming With Coordination Structures
Parallel programs display two fundamentally different kinds of execution behavior: synchronous and asynchronous.Some methodologies, such as distributed data structures, are best suited to the construction of asynchronous programs.In this paper, we propose a methodology for synchr…