A unified approach to solving seven programming problems (functional pearl)
We present seven programming challenges in Racket, and an elegant, unified approach to solving them using constraint logic programming in miniKanren.
1,066 papers · page 18 of 54
Scaling up functional programming education: under the hood of the OCaml MOOC
This article describes the key innovations used in the massive open online course ``Introduction to Functional Programming using OCaml'' that has run since the fall semester of 2015. A fully in-browser development environment with an integrated grader provides an exceptional leve…
Gradual typing with union and intersection types
We propose a type system for functional languages with gradual types and set-theoretic type connectives and prove its soundness. In particular, we show how to lift the definition of the domain and result type of an application from non-gradual types to gradual ones and likewise f…
Kami: a platform for high-level parametric hardware specification and its modular verification
It has become fairly standard in the programming-languages research world to verify functional programs in proof assistants using induction, algebraic simplification, and rewriting. In this paper, we introduce Kami, a Coq library that enables similar expressive and modular reason…
Local refinement typing
We introduce the FUSION algorithm for local refinement type inference, yielding a new SMT-based method for verifying programs with polymorphic data types and higher-order functions. FUSION is concise as the programmer need only write signatures for (externally exported) top-level…
Abstracting definitional interpreters (functional pearl)
In this functional pearl, we examine the use of definitional interpreters as a basis for abstract interpretation of higher-order programming languages. As it turns out, definitional interpreters, especially those written in monadic style, can provide a nice basis for a wide varie…
No-brainer CPS conversion (functional pearl)
Algorithms that convert direct-style λ-calculus terms to their equivalent terms in continuation-passing style (CPS) typically introduce so-called “administrative redexes:” useless artifacts of the conversion that must be cleaned up by a subsequent pass over the result to reduce t…
A metaprogramming framework for formal verification
We describe the metaprogramming framework currently used in Lean, an interactive theorem prover based on dependent type theory. This framework extends Lean's object language with an API to some of Lean's internal structures and procedures, and provides ways of reflecting object-l…
Generic functional parallel algorithms: scan and FFT
Parallel programming, whether imperative or functional, has long focused on arrays as the central data type. Meanwhile, typed functional programming has explored a variety of data types, including lists and various forms of trees. Generic functional programming decomposes these d…
Compiling to categories
It is well-known that the simply typed lambda-calculus is modeled by any cartesian closed category (CCC). This correspondence suggests giving typed functional programs a variety of interpretations, each corresponding to a different category. A convenient way to realize this idea …
How to prove your calculus is decidable: practical applications of second-order algebraic theories and computation
We present a general methodology of proving the decidability of equational theory of programming language concepts in the framework of second-order algebraic theories. We propose a Haskell-based analysis tool SOL, Second-Order Laboratory, which assists the proofs of confluence an…
On polymorphic gradual typing
We study an extension of gradual typing—a method to integrate dynamic typing and static typing smoothly in a single language—to parametric polymorphism and its theoretical properties, including conservativity of typing and semantics over both statically and dynamically typed lang…
Gradual session types
Session types are a rich type discipline, based on linear types, that lift the sort of safety claims that come with type systems to communications. However, web-based applications and micro services are often written in a mix of languages, with type disciplines in a spectrum betw…
Better living through operational semantics: an optimizing compiler for radio protocols
Software-defined radio (SDR) promises to bring the flexibility and rapid iterative workflow of software to radio protocol design. Many factors make achieving this promise challenging, not least of which are the high data rates and timing requirements of real-world radio protocols…
Chaperone contracts for higher-order sessions
Contracts have proved to be an effective mechanism that helps developers in identifying those modules of a program that violate the contracts of the functions and objects they use. In recent years, sessions have established as a key mechanism for realizing inter-module communicat…
Effect-driven QuickChecking of compilers
How does one test a language implementation with QuickCheck (aka. property-based testing)? One approach is to generate programs following the grammar of the language. But in a statically-typed language such as OCaml too many of these candidate programs will be rejected as ill-typ…
Constrained type families
We present an approach to support partiality in type-level computation without compromising expressiveness or type safety. Existing frameworks for type-level computation either require totality or implicitly assume it. For example, type families in Haskell provide a powerful, mod…
Symbolic conditioning of arrays in probabilistic programs
Probabilistic programming systems make machine learning more modular by automatinginference. Recent work by Shan and Ramsey makes inference more modular by automatingconditioning. Their technique uses a symbolic program transformation that treats conditioning generally via the me…
Parametric quantifiers for dependent type theory
Polymorphic type systems such as System F enjoy the parametricity property: polymorphic functions cannot inspect their type argument and will therefore apply the same algorithm to any type they are instantiated on. This idea is formalized mathematically in Reynolds's theory of re…
Verifying efficient function calls in CakeML
We have designed an intermediate language (IL) for the CakeML compiler that supports the verified, efficient compilation of functions and calls. Verified compilation steps include batching of multiple curried arguments, detecting calls to statically known functions, and specialis…