916 papers · page 4 of 46
Abstract We present the Kripke-style modal type theory, Mint , which combines dependent types and the necessity modality. It extends the Kripke-style modal lambda-calculus by Pfenning and Davies to the full Martin-Löf type theory. As such it encompasses dependently typed variants…
Abstract Programming language semantics is an important topic in theoretical computer science, but one that beginners often find challenging. This article provides a tutorial introduction to the subject, in which the language of integers and addition is used as a minimal setting …
series editor for further details.
series editor for further details.
Abstract This paper describes a purely functional library for computing level- p -complexity of Boolean functions and applies it to two-level iterated majority. Boolean functions are simply functions from n bits to one bit, and they can describe digital circuits, voting systems, …
Abstract Behavioral software contracts allow programmers to strengthen the obligations and promises that they express with conventional types. They lack expressive power, though, when it comes to invariants that hold across several function calls. Trace contracts narrow this expr…
Abstract Featherweight Generic Go (FGG) is a minimal core calculus modeling the essential features of the programming language Go. It includes support for overloaded methods, interface types, structural subtyping, and generics. The most straightforward semantic description of the…
Abstract This pearl defines a translation from well-typed lambda terms to combinatory logic, where both the preservation of types and the correctness of the translation are enforced statically.
Abstract Bidirectional transformations (BXs) are a mechanism for maintaining consistency between multiple representations of related data. The lens framework, which usually constructs BXs from lens combinators, has become the mainstream approach to BX programming because of its m…
Abstract We implement extraction of Coq programs to functional languages based on MetaCoq’s certified erasure. We extend the MetaCoq erasure output language with typing information and use it as an intermediate representation, which we call ${\lambda^T_\square}$ . We complement t…
Abstract Functional reactive programming (FRP) provides a high-level interface for implementing reactive systems in a declarative manner. However, this high-level interface has to be carefully reigned in to ensure that programs can in fact be executed in practice. Specifically, o…
Abstract Gradual typing allows programs to enjoy the benefits of both static typing and dynamic typing. While it is often desirable to migrate a program from more dynamically typed to more statically typed or vice versa, gradual typing itself does not provide a way to facilitate …
Abstract In this paper, we introduce a tiered-priority scheme for a synchronous message-passing language with support for selective communication and first-class communication protocols. Crucially, our scheme allows higher priority threads to communicate with lower priority threa…
Abstract A standard informal method for analyzing the asymptotic complexity of a program is to extract a recurrence that describes its cost in terms of the size of its input and then to compute a closed-form upper bound on that recurrence. We give a formal account of that method …
Abstract Fold–unfold lemmas complement the rewrite tactic in the Coq Proof Assistant to reason about recursive functions, be they defined locally or globally. Each of the structural cases gives rise to a fold–unfold lemma that equates a call to this function in that case with the…
Abstract The Robert Harper Festschrift includes articles by three of Bob’s students and colleagues—Karl Crary, Andrzej Filinski, and Jonathan Sterling. Each of these articles touches on themes that are central to Bob’s research: module system design, proof-directed program develo…
The name has also been used for Steinitz numbers, or for numbers of the form 10 4n , both otherwise unconnected with the super-naturals described here.2 Defined in Numeric.Natural, a basic Haskell library. 3 In Haskell, symbolic data constructors, which are infix by default, must…
Many students complete PhDs in functional programming each year. As a service to the community, twice per year the Journal of Functional Programming publishes the abstracts from PhD dissertations completed during the previous year. The abstracts are made freely available on the J…
A dissertation is eligible for inclusion if parts of it have or could have appeared in JFP, that is, if it is in the general area of functional programming.The abstracts are not reviewed.