Proving Properties of Lazy Functional Programs with Sparkle (2009)
Maarten De Mol, Marko Van Eekelen, Rinus Plasmeijer
Abstract. This tutorial paper aims to provide the necessary expertise for working with the proof assistant Sparkle, which is dedicated to the lazy functional programming language Clean. The purpose...
AHA: Amortized Heap Space Usage Analysis – Project Paper – (2009)
Marko Van Eekelen, Olha Shkaravska, Ron Van Kesteren, Bart Jacobs, Erik Poll, Sjaak Smetsers
Abstract: This paper introduces AHA, an NWO-funded2 344K Euro project involving research into an amortized analysis of heap-space usage by functional and imperative programs. Amortized analysis is a...
Henk Barendregt, Erik Barendsen, Jon Barwise, Johan Van Benthem, Andreas Blass, Wil Dekkers, ...
Abstract. One of the most important contributions of A. Church to logic is his invention of the lambda calculus. We present the genesis of this theory and its two major areas of application: the...
Type Checking and Weak Type Inference for Polynomial Size Analysis of First-Order Functions (2008)
Olha Shkaravska, Ron Van Kesteren, Marko Van Eekelen
Abstract. We present a size-aware type system for first-order shapely functions. Here, a function is called shapely when the size of the result is determined exactly by a polynomial in the sizes of...
Proof Tool Support for Explicit Strictness (2008)
Marko Van Eekelen, Maarten De Mol
Abstract. In programs written in lazy functional languages such as for example Clean and Haskell, the programmer can choose freely whether particular subexpressions will be evaluated lazily (the...
Chapter 1 Induction and Co-Induction in Sparkle (2008)
Leonard Lensink, Marko Van Eekelen
Abstract: Sparkle is a proof assistant designed for the lazy functional programming language Clean. It is designed to facilitate proofs of first order logical predicates on existing and newly written...
AHA: Amortized Heap Space Usage Analysis – Project Paper – (2008)
Marko Van Eekelen, Olha Shkaravska, Ron Van Kesteren, Bart Jacobs, Erik Poll, Sjaak Smetsers
This paper introduces AHA, an NWO-funded 1 344K Euro research project involving research into an amortized analysis of heap-space usage by functional and imperative programs. Amortized analysis is a...
Mixed Lazy/Strict Graph Semantics (2008)
Marko Van Eekelen, Maarten De Mol
Abstract. Explicitly enforcing strictness is often used by functional programmers as an important tool for making applications fit time and space efficiency requirements. Few functional programmers...
GEC: a toolkit for Generic Rapid Prototyping of Type Safe Interactive Applications (2008)
Peter Achten, Marko Van Eekelen, Rinus Plasmeijer, Arjen Van Weelden
Abstract. GUI programming is notoriously tedious. By using generic functions that create Graphical Editor Components (GECs), it becomes possible to define user interfaces without any knowledge of low...
language using mixed lazy/strict (2008)
Marko Van Eekelen, Maarten De Mol
about explicit strictness in a lazy
Peter Achten, Marko Van Eekelen, Rinus Plasmeijer
In slightly less than two decades Graphical User Interfaces (GUI) have become standard in presenting the user a pleasant and intuitive interface to software applications. Two major paradigms have...
An Arrow Based Semantics for Interactive Applications (2008)
Peter Achten, Marko Van Eekelen, Maarten De Mol, Rinus Plasmeijer
Interactive applications, whether they run on the desktop or as a web application, can be considered to be collections of interconnected editors that allow users to manipulate data. This is the view...
ABSTRACT Arrows for Generic Graphical Editor Components (2008)
Peter Achten, Marko Van Eekelen, Rinus Plasmeijer, Arjen Van Weelden
GUI programming is hard, even for prototyping purposes.
GEC: a toolkit for Generic Rapid Prototyping of Type Safe Interactive Applications (2008)
Peter Achten, Marko Van Eekelen, Rinus Plasmeijer, Arjen Van Weelden
GUI programming is notoriously tedious. By using generic functions that create Graphical Editor Components (GECs), it becomes possible to define user interfaces without any knowledge of low level I/O...
language using mixed lazy/strict (2007)
Marko Van Eekelen, Maarten De Mol
about explicit strictness in a lazy
Henk Barendregt, Erik Barendsen, Jon Barwise, Johan Van Benthem, Andreas Blass, Wil Dekkers, ...
Abstract. One of the most important contributions of A. Church to logic is his invention of the lambda calculus. We present the genesis of this theory and its two major areas of application: the...
Mobile Resource Guarantees (project evaluation paper) (2007)
MOMIGLIANO, ALBERTO, Marko Van Eekelen
Mobile Resource Guarantees (project evaluation paper) / D. Sannella, M. Hofmann, D.Aspinall, S. Gilmore, I. Stark, L. Beringer, H.-W. Loidl, K. MacKenzie, A. Momigliano, O. Shkaravska. - In: Trends...
Eekelen. Polynomial size analysis of first-order functions (2007)
Olha Shkaravska, Ron Van Kesteren, Marko Van Eekelen
Abstract. We present a size-aware type system for first-order shapely function definitions. Here, a function definition is called shapely when the size of the result is determined exactly by a...
GEC: A Toolkit for Generic Rapid Prototyping of Type Safe Interactive Applications (2005)
Peter Achten, Marko Van Eekelen, Rinus Plasmeijer, Arjen Van Weelden
Programming GUIs with conventional GUI APIs is notoriously tedious. In these notes we present the GEC toolkit in which the programmer can create user interfaces without any knowledge of lowlevel I/O...
There and Back Again: Arrows for Invertible Programming (2005)
Artem Alimarine, Sjaak Smetsers, Arjen Van Weelden, Marko Van Eekelen, Rinus Plasmeijer
Invertible programming occurs in the area of data conversion where it is required that the conversion in one direction is the inverse of the other. For that purpose, we introduce bidirectional arrows...
AHA Amortized Heap Space Usage Analysis (2005)
Marko Van Eekelen, Bart Jacobs, Erik Poll, Sjaak Smetsers
project involves research into an amortized analysis of heap-space usage by functional and imperative programs. Estimating heap consumption is an active research area since it becomes more and more...
Compositional Model-Views with Generic Graphical User Interfaces (2004)
P. Achten, M. Van Eekelen, R. Plasmeijer, Peter Achten, Marko Van Eekelen, Rinus Plasmeijer
Abstract. Creating GUI programs is hard even for prototyping purposes. Using the model-view paradigm makes it somewhat simpler since the model-view paradigm dictates that the model contains no GUI...
Weelden. Automatic Generation of Editors for Higher-Order Data Structures (2004)
P. Achten, M. Van Eekelen, R. Plasmeijer, A. Van Weelden, Peter Achten, Marko Van Eekelen, ...
Abstract. With generic functional programming techniques, we have eased GUI programming by constructing a programming toolkit with which one can create GUIs in an abstract and compositional way,...
Arrows for Generic Graphical Editor Components (2004)
Achten Van Eekelen, P. Achten, M. Van Eekelen, R. Plasmeijer, A. Van Weelden, Peter Achten, ...
GUI programming is hard, even for prototyping purposes. In this paper we present the Graphical Editor Component toolkit in which GUIs can be created in an abstract and compositional way. The basic...
Compositional Model-Views with Generic Graphical User Interfaces (2004)
Peter Achten, Marko Van Eekelen, Rinus Plasmeijer
Creating GUI programs is hard even for prototyping purposes.
Automatic Generation of Editors for Higher-Order Data Structures (2004)
Peter Achten, Marko Van Eekelen, Rinus Plasmeijer, Arjen Van Weelden
With generic functional programming techniques, we have eased GUI programming by constructing a programming toolkit with which one can create GUIs in an abstract and compositional way, using...
Automatic Generation of Editors for Higher-Order Data Structures (2004)
Peter Achten, Marko Van Eekelen, Rinus Plasmeijer, Arjen Van Weelden
With generic functional programming techniques, we have eased GUI programming by constructing a programming toolkit with which one can create GUIs in an abstract and compositional way, using...
Generic Graphical Editor, Peter Achten, Marko Van Eekelen, Rinus Plasmeijer, Arjen Van Weelden
GUI programming is hard, even for prototyping purposes. In this paper we present the Graphical Editor Component toolkit in which GUIs can be created in an abstract and compositional way. The basic...
Compositional Model-Views with Generic Graphical User Interfaces (2004)
Peter Achten, Marko Van Eekelen, Rinus Plasmeijer
Abstract. Creating GUI programs is hard even for prototyping purposes. Using the model-view paradigm makes it somewhat simpler since the model-view paradigm dictates that the model contains no GUI...
Arrows for Generic Graphical Editor Components (2004)
Peter Achten Marko, Marko Van Eekelen, Rinus Plasmeijer, Arjen Van Weelden
GUI programming is hard, even for prototyping purposes. In this paper we present the Graphical Editor Component toolkit in which GUIs can be created in an abstract and compositional way. The basic...
Generic Graphical User Interfaces (2003)
Peter Achten, Marko Van Eekelen, Rinus Plasmeijer
Abstract. It is important to be able to program GUI applications in a fast and easy manner. Current GUI tools for creating visually attractive applications offer limited functionality. In this paper...
Generic Graphical User Interfaces (2003)
Peter Achten, Marko Van Eekelen, Rinus Plasmeijer
Abstract. It is important to be able to program GUI applications in a fast and easy manner. Current GUI tools for creating visually attractive applications oer limited functionality. In this paper we...
Generic Graphical User Interfaces (2003)
Peter Achten, Marko Van Eekelen, Rinus Plasmeijer
It is important to be able to program GUI applications in a fast and easy manner. Current GUI tools for creating visually attractive applications o#er limited functionality. In this paper we...
Generic Graphical User Interfaces (2003)
Peter Achten, Marko Van Eekelen, Rinus Plasmeijer
Abstract. It is important to be able to program GUI applications in a fast and easy manner. Current GUI tools for creating visually attractive applications offer limited functionality. In this paper...
Table of Contents TABLE OF CONTENTS III (2002)
Rinus Plasmeijer, Marko Van Eekelen, Preface I
Version 2.1
Theorem proving for functional programmers - Sparkle: A functional theorem prover (2001)
Maarten De Mol, Marko Van Eekelen, Rinus Plasmeijer
Abstract. Sparkle is a new theorem prover written in and specialized for the functional programming language Clean. It is mainly intended to be used by programmers for proving properties of parts of...
Theorem proving for functional programmers - Sparkle: A functional theorem prover (2001)
Maarten De Mol, Marko Van Eekelen, Rinus Plasmeijer
Abstract. Sparkle is a new theorem prover written and specialized in the functional programming language Clean. It is in the first place intended to be used by programmers on small parts of...
Polygonizing Implicit Surfaces in a Purely Functional Way (2000)
Pieter Koopman, Marko Van Eekelen, Rinus Plasmeijer
Abstract. Implicit surfaces are dened by a real valued function. They can easily be dened and manipulated and have therefore gained great popularity in computer graphics. This paper presents a purely...
Graph Rewriting Semantics for Functional Programming Languages (1996)
Marko Van Eekelen, Sjaak Smetsers, Rinus Plasmeijer
. The lambda calculus forms without any question *the* theoretical backbone of functional programming languages. For the design and implementation of the lazy functional language Concurrent Clean we...
Sjaak Smetsers, Erik Barendsen, Marko Van Eekelen, Rinus Plasmeijer
In this paper we present a type system for graph rewrite systems: uniqueness typing . It employs usage information to deduce whether an object is `unique' at a certain moment, i.e. is only...
FunSheet: A Functional Spreadsheet (1994)
Walter De Hoon, Luc Rutten, Marko Van Eekelen
It has been claimed that recent developments in the research on efficiency of code generation and on graphical input/output interfacing have made it possible to use a functional language to write...
The Functional Strategy and Transitive Term Rewriting Systems (1993)
Yoshihito Toyama, Sjaak Smetsers, Marko Van Eekelen, Rinus Plasmeijer
The functional strategy has been widely used implicitly (Haskell, Miranda, Lazy ML) and explicitly (Clean) as an efficient, intuitively easy to understand reduction strategy for term (or graph)...
Eric Nöcker, Sjaak Smetsers, Marko Van Eekelen, Rinus Plasmeijer
Concurrent Clean is an experimental, lazy, higher-order parallel functional programming language based on term graph rewriting. An important difference with other languages is that in Clean graphs...