Related papers: Toward Hole-Driven Development with Liquid Haskell
Cyp (Check Your Proofs) (Durner and Noschinski 2013; Traytel 2019) verifies proofs about Haskell-like programs. We extended Cyp with a pattern matcher for programs and proof terms, and a type checker. This allows to use Cyp for auto-grading…
Datatype-generic programming increases program abstraction and reuse by making functions operate uniformly across different types. Many approaches to generic programming have been proposed over the years, most of them for Haskell, but…
Dependently-typed host languages empower users to verify a wide range of properties of embedded languages and programs written in them. Designers of such embedded languages are faced with a difficult choice between using a shallow or a deep…
Bugs that are detected earlier during the development lifecycle are easier and cheaper to fix, whereas bugs that are found during production are difficult and expensive to address, and may have dire consequences. Type systems are…
In this paper, we prove correctness of parallelizing a string matcher using Haskell as a theorem prover. We use refinement types to specify correctness properties, Haskell terms to express proofs and Liquid Haskell to check correctness of…
Linear type systems have a long and storied history, but not a clear path forward to integrate with existing languages such as OCaml or Haskell. In this paper, we study a linear type system designed with two crucial properties in mind:…
Formal reasoning about the time complexity of algorithms and data structures is usually done in interactive theorem provers like Isabelle/HOL. This includes reasoning about amortized time complexity which looks at the worst case performance…
We propose an amortized analysis that approximates the resource usage of a Haskell expression. Using the plugin API of GHC, we convert the Haskell code into a simplified representation called GHC Core. We then apply a type-based system…
The R programming language is widely used in large-scale data analyses. It contains especially rich built-in support for dealing with vectors, arrays, and matrices. These operations feature prominently in the applications that form R's…
In recent years we have explored using Haskell alongside a traditional mathematical formalism in our large-enrolment university course on topics including logic and formal languages, aiming to offer our students a programming perspective on…
We consider the problem of type-directed component based synthesis where, given a set of (typed) components and a query type, the goal is to synthesize a term that inhabits the query. Classical approaches based on proof search in…
This dissertation introduces executable refinement types, which refine structural types by semi-decidable predicates, and establishes their metatheory and accompanying implementation techniques. These results are useful for undecidable type…
Logic programming languages present clear advantages in terms of declarativeness and conciseness. However, the ideas of logic programming have been met with resistance in other programming communities, and have not generally been adopted by…
Refinement types enrich a language's type system with logical predicates that circumscribe the set of values described by the type, thereby providing software developers a tunable knob with which to inform the type system about what…
This document specifies a core version of the type theory implemented in the Cedille tool. Cedille is a language for dependently typed programming and computer-checked proof. Cedille can elaborate source programs down to Cedille Core, which…
In recent years, languages like Haskell have seen a dramatic surge of new features that significantly extends the expressive power of their type systems. With these features, the challenge of kind inference for datatype declarations has…
Haskell, as implemented in the Glasgow Haskell Compiler (GHC), has been adding new type-level programming features for some time. Many of these features---chiefly: generalized algebraic datatypes (GADTs), type families, kind polymorphism,…
Probabilistic programming and the formal analysis of probabilistic algorithms are active areas of research, driven by the widespread use of randomness to improve performance. While functional correctness has seen substantial progress,…
Type classes are one of Haskell's most popular features and extend its type system with ad-hoc polymorphism. Since their conception, there were useful features that could not be offered because of the desire to offer two correctness…
Using agda2hs and ad-hoc Haskell FFI bindings, writing Qt applications in C++ with Agda- or Haskell-based backends (possibly including correctness proofs) is already possible. However, there was no repeatable methodology to do so, nor to…