916 papers · page 24 of 46
This book discusses four approaches typically used for the verification of reactive systems.However, the book is not merely a description of these four formalisms, since the existing connections between these techniques are also established.In addition, complexity results associa…
Abstract The functional programming community has shown some interest in spreadsheets, but surprisingly no one seems to have considered making a standard spreadsheet, such as Excel, work with a standard functional programming language, such as Haskell. In this paper, we show one …
Abstract We present an approach to enriching the type system of ML with a restricted form of dependent types, where type index terms are required to be drawn from a given type index language ${\cal L}$ that is completely separate from run-time programs, leading to the DML( ${\cal…
In a typing system, there are two approaches that may be taken to the notion of equality. One can use some external relation of convertibility defined on the terms of the grammar, such as -convertibility; or one can introduce a judgement form for equality into the rules of the ty…
Pure Type Systems (PTS) come in two flavours: domain-free systems with untyped $\lambda$ -abstractions (i.e. of the form $\lambda{x}.{M}$ ); and domain-free systems with typed $\lambda$ -abstractions (i.e. of the form $\lambda{x}{A}{M}$ ). Both flavours of systems are related by …
We formalize and prove the folklore theorem that the static delimited-control operators shift and reset can be simulated in terms of the dynamic delimited-control operators control and prompt. The proof is based on small-step operational semantics.
There's no maths involved. You solve the puzzle with reasoning and logic. Advice on how to play Sudoku, The Independent Newspaper
The setting is a class on functional programming. There are four students, Anne, Jack, Mary and Theo.
Even in statically typed languages it is useful to have certain invariants checked dynamically. Findler and Felleisen gave an algorithm for dynamically checking expressive higher-order types called contracts. They did not, however, give a semantics of contracts. The lack of a sem…
The Theory of Contexts is a type-theoretic axiomatization aiming to give a metalogical account of the fundamental notions of variable and context as they appear in Higher Order Abstract Syntax. In this paper, we prove that this theory is consistent by building a model based on fu…
A part of a query that will never contribute data to the query answer should be regarded as an error. This principle has been recently accepted into mainstream XML query languages, but was still waiting for a complete treatment. We provide here a precise definition for this class…
A bag (literally and mathematically!) of marbles is deemed to be mingled if all the colours of the marbles are different. Given a positive integer $k$ and a collection of $m$ marbles, our objective is to try and extract as many mingled bags as possible from the collection, where …
A huge discrepancy between theory and practice exists in one popular application area of functional programming – spreadsheets. Although spreadsheets are the most frequently used (functional) programs, they fall short of the quality level that is expected of functional programs, …
At the heart of functional programming rests the principle of referential transparency, which in particular means that a function f applied to a value x always yields one and the same value y=f(x) . This principle seems to be violated when contemplating the use of functions to de…
Among systems for creating slide presentations, the dominant ones offer essentially no abstraction capability. Slideshow represents our effort over the last several years to build an abstraction-friendly slide system with PLT Scheme. We show how functional programming is well sui…
The Ninth ACM SIGPLAN International Conference on Functional Programming (ICFP) took place on September 19–21 2004 in Snowbird, Utah. The scope of ICFP includes all languages that encourage programming with functions, with topics ranging from principles to practice, foundations t…
Region-based type systems provide programmer control over memory management without sacrificing type-safety. However, the type systems for region-based languages, such as the ML-Kit or Cyclone, are relatively complicated, and proving their soundness is non-trivial. This paper sho…
We investigate a technique from the literature, called the phantom-types technique, that uses parametric polymorphism, type constraints, and unification of polymorphic types to model a subtyping hierarchy. Hindley-Milner type systems, such as the one found in Standard ML, can be …
Every lazy functional programmer knows about the following approach to enumerating the positive rationals: generate a two-dimensional matrix (an infinite list of infinite lists), then traverse its finite diagonals (an infinite list of finite lists).
This paper introduces reFLect, a functional programming language with reflection features intended for applications in hardware design and verification. The reFLect language is strongly typed and similar to ML, but has quotation and antiquotation constructs. These may be used to …