7,482 papers · page 206 of 375
What is a basic automata-theoretic model of computation with names and fresh-name generation? We introduce Fresh-Register Automata (FRA), a new class of automata which operate on an infinite alphabet of names and use a finite number of registers to store fresh names, and to compa…
Modular languages support generative type abstraction, ensuring that an abstract type is distinct from its representation, except inside the implementation where the two are synonymous. We show that this well-established feature is in tension with the non-parametric features of n…
Sparse matrix formats are typically implemented with low-level imperative programs. The optimized nature of these implementations hides the structural organization of the sparse format and complicates its verification. We define a variable-free functional language (LL) in which e…
Bidirectional programming languages are a practical approach to the view update problem. Programs in these languages, called lenses, define both a view and an update policy - i.e., every program can be read as a function mapping sources to views as well as one mapping updated vie…
Nested data-parallelism (NDP) is a declarative style for programming irregular parallel applications. NDP languages provide language features favoring the NDP style, efficient compilation of NDP programs, and various common NDP operations like parallel maps, filters, and sum-like…
Reynolds' abstraction theorem shows how a typing judgement in System F can be translated into a relational statement (in second order predicate logic) about inhabitants of the type. We (in second order predicate logic) about inhabitants of the type. We obtain a similar result for…
We study a first-order functional language with the novel combination of the ideas of refinement type (the subset of a type to satisfy a Boolean expression) and type-test (a Boolean expression testing whether a value belongs to a type). Our core calculus can express a rich variet…
Functional programming presents several important advantages in the design, analysis and implementation of parallel algorithms:
Partial evaluation aims to improve the efficiency of a program by specialising it with respect to some known inputs. In this paper, we show that partial evaluation can be an effective and, unusually, easy to use technique for the efficient implementation of embedded domain-specif…
To fix bugs or to enhance a software system without service disruption, one has to update it dynamically during execution. Most prior dynamic software updating techniques require that the code to be changed is not running at the time of the update. However, this restriction precl…
We present a closed dependent type theory whose inductive types are given not by a scheme for generative declarations, but by encoding in a universe. Each inductive datatype arises by interpreting its description - a first-class value in a datatype of descriptions. Moreover, the …
This paper describes CFML, the first program verification tool based on characteristic formulae. Given the source code of a pure Caml program, this tool generates a logical formula that implies any valid post-condition for that program. One can then prove that the program satisfi…
We present a technique for higher-order representation of substructural logics such as linear or modal logic. We show that such logics can be encoded in the (ordinary) Logical Framework, without any linear or modal extensions. Using this encoding, metatheoretic proofs about such …
A student learning how to program learns best when the programming language and programming environment cater to her specific needs. These needs are different from the requirements of a professional programmer. Consequently, the design of teaching languages poses challenges diffe…
Existing macro systems force programmers to make a choice between clarity of specification and robustness. If they choose clarity, they must forgo validating significant parts of the specification and thus produce low-quality language extensions. If they choose robustness, they m…
A monadic parser combinator library which guarantees termination of parsing, while still allowing many forms of left recursion, is described. The library's interface is similar to those of many other parser combinator libraries, with two important differences: one is that the int…
Reasoning about program equivalence is one of the oldest problems in semantics. In recent years, useful techniques have been developed, based on bisimulations and logical relations, for reasoning about equivalence in the setting of increasingly realistic languages - languages nea…
In 1995, my team and I decided to create an outreach project that would use our research on functional programming to change the K-12 computer science curriculum. We had two different goals in mind. On the one hand, our curriculum should rely on mathematics to teach programming, …
Cody, Hazel, and Theo, two experienced Haskell programmers and an expert in automata theory, develop an elegant Haskell program for matching regular expressions: (i) the program is purely functional; (ii) it is overloaded over arbitrary semirings, which not only allows to solve t…
My talk will celebrate Robin Milner's contribution to functional programming via a combination of reminiscences about the early days of ML and speculations about its future.