916 papers · page 26 of 46
We consider a propositional spatial logic for finite trees. The logic includes $\A \Par \B$ (tree composition), $\A \,{\Guarantee}\, \B$ (the implication induced by composition), and $\Zero$ (the unit of composition). We show that the satisfaction and validity problems are equiva…
By allowing the programmer to write code that can generate code at run-time, meta-programming offers a powerful approach to program construction. For instance, meta-programming can often be employed to enhance program efficiency and facilitate the construction of generic programs…
We explore the logical underpinnings of higher-order, security-typed languages with mutable state. Our analysis is based on a logic of information flow derived from lax logic and the monadic metalanguage. Thus, our logic deals with mutation explicitly, with impurity reflected in …
We introduce a typed λ-calculus which allows the use of exceptions in the ML style. It is an extension of the system $AF_2$ of Krivine & Leivant (Krivine, 1990; Leivant, 1983). We show its main properties: confluence, strong normalization and weak subject reduction. The system sa…
This paper presents SKRIBE, a functional programming language for authoring documents, especially technical documents such as web pages, technical reports, and API documentation. Executing Skribe programs can produce documents in various formats, such as PostScript, PDF, HTML, Te…
Classical application domains of parallel computing are dominated by processing large arrays of numerical data. Whereas most functional languages focus on lists and trees rather than on arrays, S A C is tailor-made in design and in implementation for efficient high-level array pr…
In this paper, we present some experience of using the concurrent functional language Erlang to implement a distributed video-on-demand server. For performance reasons, the server is deployed in a cheap cluster made from off-the-shelf components. The demanding system requirements…
Haskell is a functional programming language whose evaluation is lazy by default. However, Haskell also provides pattern matching facilities which add a modicum of eagerness to its otherwise lazy default evaluation. This mixed or “non-strict” semantics can be quite difficult to r…
This pearl explains Church numerals, twice. The first explanation links Church numerals to Peano numerals via the well-known encoding of data types in the polymorphic λ-calculus. This view suggests that Church numerals are folds in disguise. The second explanation, which is more …
This paper proposes new syntactic inference rules which can directly extract information flow in a given typed process in the π-calculus. In the flow analysis, a flow in a process is captured as a chain of possible interactions which transform differences in behaviours from one p…
We present the Zen toolkit for morphological and phonological processing of natural languages. This toolkit is presented in literate programming style, in the Pidgin ML subset of the Objective Caml functional programming language. This toolkit is based on a systematic representat…
Type theory was invented at the beginning of the twentieth century with the aim of avoiding the paradoxes which result from the self-application of functions. $\lambda$ -calculus was developed in the early 1930s as a theory of functions. In 1940, Church added type theory to his $…
Eden extends the non-strict functional language Haskell with constructs to control parallel evaluation of processes. Although processes are defined explicitly, communication and synchronisation issues are handled in a way transparent to the programmer. In order to offer effective…
We present a rule-based framework for the development of scalable parallel high performance simulations for a broad class of scientific applications (with particular emphasis on continuum mechanics). We take a pragmatic approach to our programming abstractions by implementing str…
Staging is a programming technique for dividing the computation in order to exploit the early availability of some arguments. In the early stages the program uses the available arguments to generate, at run time, the code for the late stages. A type system for staging should ensu…
This pearl gives a discount proof of the folklore theorem that every strongly which can type any term.) The proof uses the perpetual reduction strategy which finds a longest path. This is a simplification over existing proofs that consider any longest reduction path. The choice o…
Functional programming fits well with the use of descriptive markup in HTML and XML. There is also a good fit between S-expressions in Lisp and the XML data set. These similarities are exploited in LAML which is a software package for Scheme. LAML supports exact mirrors of the th…
The parallel-functional language Eden has a non-deterministic construct, the process abstraction merge, which interleaves a set of input lists to produce a single non-deterministic list. Its non-deterministic behaviour is a consequence of its reactivity: it immediately copies to …
We introduce a quantitative approach to the analysis of distributed systems which relies on a linear operator based network semantics. A typical problem in a distributed setting is how information propagates through a network, and a typical qualitative analysis is concerned with …
A compiler structured as a small number of monolithic passes is difficult to understand and difficult to maintain. The steep learning curve is daunting, and even experienced developers find that modifying existing passes is difficult and often introduces subtle and tenacious bugs…