1,066 papers · page 29 of 54
Characteristic formulae for the verification of imperative programs
In previous work, we introduced an approach to program verification based on characteristic formulae. The approach consists of generating a higher-order logic formula from the source code of a program. This characteristic formula is constructed in such a way that it gives a sound…
Implicit self-adjusting computation for purely functional programs
Computational problems that involve dynamic data, such as physics simulations and program development environments, have been an important subject of study in programming languages. Building on this work, recent advances in self-adjusting computation have developed techniques tha…
Using camlp4 for presenting dynamic mathematics on the web: DynaMoW, an OCaml language extension for the run-time generation of mathematical contents and their presentation on the web
We report on the design and implementation of a programming tool, DynaMoW, to control interactive and incremental mathematical calculations to be presented on the web. This tool is implemented as a language extension of OCaml using Camlp4. Fragments of mathematical code written f…
On the bright side of type classes: instance arguments in Agda
We present instance arguments: an alternative to type classes and related features in the dependently typed, purely functional programming language/proof assistant Agda. They are a new, general type of function arguments, resolved from call-site scope in a type-directed way. The …
Temporal higher-order contracts
Behavioral contracts are embraced by software engineers because they document module interfaces, detect interface violations, and help identify faulty modules (packages, classes, functions, etc). This paper extends prior higher-order contract systems to also express and enforce t…
Towards a comprehensive theory of monadic effects
It has been more than 20 years since monads were proposed as a unifying concept for computational effects, in both formal semantics and functional programs. Over that period, there has been substantial incremental progress on several fronts within the ensuing research area, inclu…
Forest: a language and toolkit for programming with filestores
A filestore is a structured collection of data files housed in a conventional hierarchical file system. Many applications use filestores as a poor-man's database, and the correct execution of these applications requires that the collection of files, directories, and symbolic link…
Frenetic: a network programming language
Modern networks provide a variety of interrelated services including routing, traffic monitoring, load balancing, and access control. Unfortunately, the languages used to program today's networks lack modern features - they are usually defined at the low level of abstraction supp…
Linearity and PCF: a semantic insight!
Linearity is a multi-faceted and ubiquitous notion in the analysis and the development of programming language concepts. We study linearity in a denotational perspective by picking out programs that correspond to linear functions between coherence spaces.
Parametric polymorphism and semantic subtyping: the logical connection
We consider a type algebra equipped with recursive, product, function, intersection, union, and complement types together with type variables and implicit universal quantification over them. We consider the subtyping relation recently defined by Castagna and Xu over such type exp…
Geometry of synthesis iv: compiling affine recursion into static hardware
Abramsky's Geometry of Interaction interpretation (GoI) is a logical-directed way to reconcile the process and functional views of computation, and can lead to a dataflow-style semantics of programming languages that is both operational (i.e. effective) and denotational (i.e. ind…
Just do it: simple monadic equational reasoning
One of the appeals of pure functional programming is that it is so amenable to equational reasoning. One of the problems of pure functional programming is that it rules out computational effects. Moggi and Wadler showed how to get round this problem by using monads to encapsulate…
Deriving an efficient FPGA implementation of a low density parity check forward error corrector
Creating correct hardware is hard. Though there is much talk of using formal and semi-formal methods to develop designs and implementations, in practice most implementations are written without the support of any formal or semi-formal methodology. Having such a methodology brings…
How to make ad hoc proof automation less ad hoc
Most interactive theorem provers provide support for some form of user-customizable proof automation. In a number of popular systems, such as Coq and Isabelle, this automation is achieved primarily through tactics, which are programmed in a separate language from that of the prov…
Modular verification of preemptive OS kernels
Most major OS kernels today run on multiprocessor systems and are preemptive: it is possible for a process running in the kernel mode to get descheduled. Existing modular techniques for verifying concurrent code are not directly applicable in this setting: they rely on scheduling…
Proving the unique fixed-point principle correct: an adventure with category theory
Say you want to prove something about an infinite data-structure, such as a stream or an infinite tree, but you would rather not subject yourself to coinduction. The unique fixed-point principle is an easy-to-use, calculational alternative. The proof technique rests on the fact t…
Typed self-interpretation by pattern matching
Self-interpreters can be roughly divided into two sorts: self-recognisers that recover the input program from a canonical representation, and self-enactors that execute the input program. Major progress for statically-typed languages was achieved in 2009 by Rendel, Ostermann, and…
A semantic model for graphical user interfaces
We give a denotational model for graphical user interface (GUI) programming using the Cartesian closed category of ultrametric spaces. The ultrametric structure enforces causality restrictions on reactive systems and allows well-founded recursive definitions by a generalization o…
Functional modelling of musical harmony: an experience report
Music theory has been essential in composing and performing music for centuries. Within Western tonal music, from the early Baroque on to modern-day jazz and pop music, the function of chords within a chord sequence can be explained by harmony theory. Although Western tonal harmo…