Abstract Interpretation of Higher Order Functions using Concrete Data Structures (Summary)

1993 ◽  
pp. 57-61 ◽  
Author(s):  
A. B. Ferguson ◽  
John Hughes
Keyword(s):  
Data Structures ◽  
Abstract Interpretation ◽  
Higher Order ◽  
Higher Order Functions

Functional programming with the FC++ library

2004 ◽  
Vol 14 (4) ◽  
pp. 429-472 ◽  
Author(s):  
BRIAN MCNAMARA ◽  
YANNIS SMARAGDAKIS
Keyword(s):  
Data Structures ◽  
Functional Programming ◽  
Higher Order ◽  
Performance Comparison ◽  
Type Inference ◽  
High Complexity ◽  
Time Performance ◽  
Order Of Magnitude ◽  
Supporting Functional ◽  
Higher Order Functions

We describe the FC++ library, a rich library supporting functional programming in C++. Prior approaches to encoding higher order functions in C++ have suffered with respect to polymorphic functions from either lack of expressiveness or high complexity. In contrast, FC++ offers full and concise support for higher-order polymorphic functions through a novel use of C++ type inference. The FC++ library has a number of useful features, including a generalized mechanism to implement currying in C++, a “lazy list” class which enables the creation of “infinite data structures”, a subtype polymorphism facility, and an extensive library of useful functions, including a large part of the Haskell Standard Prelude. The FC++ library has an efficient implementation. We show the results of a number of experiments which demonstrate the value of optimizations we have implemented. These optimizations have improved the run-time performance by about an order of magnitude for some benchmark programs that make heavy use of FC++ lazy lists. We also make an informal performance comparison with similar programs written in Haskell.

A syntactic method for finding least fixed points of higher-order functions over finite domains

1997 ◽  
Vol 7 (4) ◽  
pp. 357-394
Author(s):  
TYNG-RUEY CHUANG ◽  
BENJAMIN GOLDBERG
Keyword(s):  
Fixed Point ◽  
Fixed Points ◽  
Normal Forms ◽  
Abstract Interpretation ◽  
Higher Order ◽  
Semantic Domain ◽  
Recent Developments ◽  
Strictness Analysis ◽  
Finite Domains ◽  
Higher Order Functions

This paper describes a method for finding the least fixed points of higher-order functions over finite domains using symbolic manipulation. Fixed point finding is an essential component in the calculation of abstract semantics of functional programs, providing the foundation for program analyses based on abstract interpretation. Previous methods for fixed point finding have primarily used semantic approaches, which often must traverse large portions of the semantic domain even for simple programs. This paper provides the theoretical framework for a syntax-based analysis that is potentially very fast. The proposed syntactic method is based on an augmented simply typed lambda calculus where the symbolic representation of each function produced in the fixed point iteration is transformed to a syntactic normal form. Normal forms resulting from successive iterations are then compared syntactically to determine their ordering in the semantic domain, and to decide whether a fixed point has been reached. We show the method to be sound, complete and compositional. Examples are presented to show how this method can be used to perform strictness analysis for higher-order functions over non-flat domains. Our method is compositional in the sense that the strictness property of an expression can be easily calculated from those of its sub-expressions. This is contrary to most strictness analysers, where the strictness property of an expression has to be computed anew whenever one of its subexpressions changes. We also compare our approach with recent developments in strictness analysis.

Fixed points and frontiers: a new perspective

1991 ◽  
Vol 1 (1) ◽  
pp. 91-120 ◽  
Author(s):  
Sebastian Hunt ◽  
Chris Hankin
Keyword(s):  
Fixed Points ◽  
Abstract Interpretation ◽  
Higher Order ◽  
Upper And Lower Bounds ◽  
Elegant Method ◽  
Computation Of Fixed Points ◽  
New Perspective ◽  
New Formulation ◽  
Intractable Problem ◽  
Higher Order Functions

AbstractAbstract interpretation is the collective name for a family of semantics-based techniques for compile-time analysis of programs. One of the most costly operations in automating such analyses is the computation of fixed points. The frontiers algorithm is an elegant method, invented by Chris Clack and Simon Peyton Jones, which addresses this issue.In this article we present a new approach to the frontiers algorithm based on the insight that frontiers represent upper and lower subsets of a function's argument domain. This insight leads to a new formulation of the frontiers algorithm for higher-order functions, which is considerably more concise than previous versions.We go on to argue that for many functions, especially in the higher-order case, finding fixed points is an intractable problem unless the sizes of the abstract domains are reduced. We show how the semantic machinery of abstract interpretation allows us to place upper and lower bounds on the values of fixed points in large lattices by working within smaller ones.

scholarly journals A logical analysis of aliasing in imperative higher-order functions

2007 ◽  
Vol 17 (4-5) ◽  
pp. 473-546 ◽  
Author(s):  
MARTIN BERGER ◽  
KOHEI HONDA ◽  
NOBUKO YOSHIDA
Keyword(s):  
Data Structures ◽  
Building Blocks ◽  
Higher Order ◽  
Logical Analysis ◽  
Logical Status ◽  
Open Issue ◽  
Higher Order Functions ◽  
Structural Reasoning

AbstractWe present a compositional programme logic for call-by-value imperative higher-order functions with general forms of aliasing, which can arise from the use of reference names as function parameters, return values, content of references and parts of data structures. The programme logic extends our earlier logic for alias-free imperative higher-order functions with new operators which serve as building blocks for clean structural reasoning about programms and data structures in the presence of aliasing. This has been an open issue since the pioneering work by Cartwright–Oppen and Morris twenty-five years ago. We illustrate usage of the logic for description and reasoning through concrete examples including a higher-order polymorphic Quicksort. The logical status of the new operators is clarified by translating them into (in)equalities of reference names.

scholarly journals Sharing analysis in the Pawns compiler

2015 ◽  
Author(s):  
Lee Naish
Keyword(s):  
Programming Language ◽  
Data Structures ◽  
Source Code ◽  
Higher Order ◽  
Declarative Programming ◽  
Data Types ◽  
Shared Data ◽  
Algebraic Data Types ◽  
Higher Order Functions

Pawns is a programming language under development which supports algebraic data types, polymorphism, higher order functions and "pure" declarative programming. It also supports impure imperative features including destructive update of shared data structures via pointers, allowing significantly increased efficiency for some operations. A novelty of Pawns is that all impure "effects" must be made obvious in the source code and they can be safely encapsulated in pure functions in a way that is checked by the compiler. Execution of a pure function can perform destructive updates on data structures which are local to or eventually returned from the function without risking modification of the data structures passed to the function. This paper describes the sharing analysis which allows impurity to be encapsulated. Aspects of the analysis are similar to other published work, but in addition it handles explicit pointers and destructive update, higher order functions including closures and pre- and postconditions concerning sharing for functions.

scholarly journals Sharing analysis in the Pawns compiler

2015 ◽  
Author(s):  
Lee Naish
Keyword(s):  
Programming Language ◽  
Data Structures ◽  
Source Code ◽  
Higher Order ◽  
Declarative Programming ◽  
Data Types ◽  
Shared Data ◽  
Algebraic Data Types ◽  
Higher Order Functions

Pawns is a programming language under development that supports algebraic data types, polymorphism, higher order functions and "pure" declarative programming. It also supports impure imperative features including destructive update of shared data structures via pointers, allowing significantly increased efficiency for some operations. A novelty of Pawns is that all impure "effects" must be made obvious in the source code and they can be safely encapsulated in pure functions in a way that is checked by the compiler. Execution of a pure function can perform destructive updates on data structures that are local to or eventually returned from the function without risking modification of the data structures passed to the function. This paper describes the sharing analysis which allows impurity to be encapsulated. Aspects of the analysis are similar to other published work, but in addition it handles explicit pointers and destructive update, higher order functions including closures and pre- and post-conditions concerning sharing for functions.

scholarly journals Sharing analysis in the Pawns compiler

2015 ◽  
Author(s):  
Lee Naish
Keyword(s):  
Programming Language ◽  
Data Structures ◽  
Source Code ◽  
Higher Order ◽  
Declarative Programming ◽  
Data Types ◽  
Shared Data ◽  
Algebraic Data Types ◽  
Higher Order Functions

Pawns is a programming language under development that supports algebraic data types, polymorphism, higher order functions and "pure" declarative programming. It also supports impure imperative features including destructive update of shared data structures via pointers, allowing significantly increased efficiency for some operations. A novelty of Pawns is that all impure "effects" must be made obvious in the source code and they can be safely encapsulated in pure functions in a way that is checked by the compiler. Execution of a pure function can perform destructive updates on data structures that are local to or eventually returned from the function without risking modification of the data structures passed to the function. This paper describes the sharing analysis which allows impurity to be encapsulated. Aspects of the analysis are similar to other published work, but in addition it handles explicit pointers and destructive update, higher order functions including closures and pre- and post-conditions concerning sharing for functions.

Sign in / Sign up

Export Citation Format

Share Document