| Abstraction and Invariance for Algebraically Indexed Types |
2013 |
202 |
Reynolds’ relational parametricity provides a powerful way to reason about programs in terms of invariance under changes of data representation. A dazzling array of applications of Reynolds’ theory exists, exploiting invariance to yield “free theorem... |
| Bifibrational Functorial Semantics For Parametric Polymorphism |
2015 |
241 |
Reynolds’ theory of parametric polymorphism captures the invariance of polymorphically typed programs under change of data representation. Semantically, reflexive graph categories and fibrations are both known to give a categorical understanding of p... |
| A Family Of Syntactic Logical Relations For The Semantics Of Haskell-Like Languages |
2009 |
291 |
Logical relations are a fundamental and powerful tool for reasoning about programs in languages with parametric polymorphism. Logical relations suitable for reasoning about observational behavior in polymorphic calculi supporting various programming ... |
| Fibrational Induction Meets Effects |
2016 |
290 |
This paper provides several induction rules that can be used to prove properties of effectful data types. Our results are semantic in nature and build upon Hermida and Jacobs’ fibrational formulation of induction for polynomial data types and its ext... |
| Fibrational Induction Rules for Initial Algebras |
2010 |
228 |
This paper provides an induction rule that can be used to prove properties of data structures whose types are inductive, i.e., are carriers of initial algebras of functors. Our results are semantic in nature and are inspired by Hermida and Jacobs’ el... |
| Foundations For Structured Programming With GADTs |
2008 |
467 |
GADTs are at the cutting edge of functional programming and be-come more widely used every day. Nevertheless, the semantic foundations underlying GADTs are not well understood. In this paper we solve this problem by showing that the standard theory o... |
| Fusing Logic And Control With Local Transformations: An Example Optimization |
2001 |
167 |
Programming supports the separation of logical concerns from issues of control in program construction. While this separation of concerns leads to reduced code size and increased reusability of code, its main disadvantage is the computational overhea... |
| A Generalization of Short-Cut Fusion and Its Correctness Proof |
2002 |
230 |
Short-cut fusion is a program transformation technique that uses a single local transformation - called the foldr build rule - to remove certain intermediate lists from modularly constructed functional programs. Arguments that short-cut fusion is cor... |
| Generic Fibrational Induction |
2012 |
339 |
This paper provides an induction rule that can be used to prove properties of data structures whose types are inductive, i.e., are carriers of initial algebras of functors. Our results are semantic in nature and are inspired by Hermida and Jacobs’ el... |
| A Generic Operational Metatheory for Algebraic Effects |
2010 |
368 |
We provide a syntactic analysis of contextualpreorder and equivalence for a polymorphic programminglanguage with effects. Our approach applies uniformly acrossa range of algebraic effects, and incorporates, as instances:errors, input/output, global s... |
| Haskell Programming with Nested Types: A Principled Approach |
2009 |
721 |
Initial algebra semantics is one of the cornerstones of the theory of modern functional programming languages. For each inductive data type, it provides a Church encoding for that type, a build combinator which constructs data of that type, a fold co... |
| An Improved General E-unification Method |
1992 |
453 |
A generalization of Paramodulation is defined and shown to lead to a complete E-Unification method for arbitrary equational theories E. The method is defined in term of transformations on systems, building upon and refining results of Gallier and Sny... |
| Indexed Induction And Coinduction, Fibrationally |
2013 |
399 |
This paper extends the fibrational approach to induction and coinductionpioneered by Hermida and Jacobs, and developed by the current authors, in two keydirections. First, we present a dual to the sound induction rule for inductive types thatwe devel... |
| Interleaving Data and Effects |
2015 |
454 |
The study of programming with and reasoning about inductive datatypes such as lists and trees has benefited from the simple categorical principle of initial algebras. In initial algebra semantics, each inductive datatype is represented by an initial ... |
| Monadic Augment And Generalized Short Cut Fusion |
2007 |
177 |
Monads are commonplace programming devices that are used to uniformly structure computations;in particular, they are often used to mimic the effects of impure features suchas state, error handling, and I/O. This paper further develops the monadic pro... |
| Monadic fold, Monadic build, Monadic Short Cut Fusion |
2009 |
179 |
Abstract: Short cut fusion improves the efficiency of modularly constructed programs by eliminating intermediate data structures produced by one program component and immediately consumed by another. We define a combinator which expresses uniform pro... |
| On Proving the Correctness of Program Transformations Based on Free Theorems for Higher-order Polymorphic Calculi |
2005 |
407 |
A number of program transformations currently of interest can be derived from Wadler's "free theorems" for calculi approximately modern functional languages. Although delicate but fundamental issues arise in proving the correctness of free theorems-b... |
| Refining Inductive Types |
2012 |
221 |
Dependently typed programming languages allow sophisticated properties of data to be expressed within the type system. Of particular use in dependently typed programming are indexed types that refine data by computationally useful information. For ex... |
| A Relationally Parametric Model of Dependent Type Theory |
2014 |
392 |
Reynolds’ theory of relational parametricity captures the invariance of polymorphically typed programs under change of data representation. Reynolds’ original work exploited the typing discipline of the polymorphically typed -calculus System F, but t... |
| Selective Strictness and Parametricity in Structural Operational Semantics, Inequationally |
2007 |
316 |
Parametric polymorphism constrains the behavior of pure functional pro-grams in a way that allows the derivation of interesting theorems about them solely from their types, i.e., virtually for free. The formal background of such ‘free theorems’ is we... |
| Short Cut Fusion is Correct |
2003 |
476 |
Fusion is the process of removing intermediate data structures from modularly constructed functional programs. Short cut fusion is a particular fusion technique which uses a single, local transformation rule to fuse compositions of list-processing fu... |
| Short Cut Fusion: Proved and Improved |
2001 |
314 |
Short cut fusion is a particular program transformation technique which uses a single, local transformation — called the foldrbuild rule — to remove certain intermediate lists from modularly constructed functional programs. Arguments that short cut f... |
| Structural Resolution for Automated Verification |
2015 |
143 |
We pose a research question: Can the newly-developed structural resolution be used to extend co-inductive methods in automated theorem proving? |
| Structural Resolution for Logic Programming |
2015 |
143 |
We introduce a Three Tier Tree Calculus (T 3C) that defines in a systematic way three tiers of tree structures underlying proof search in logic programming. We use T 3C to define a new – structural –version of resolution for logic programming. |
| Warm Fusion in Stratego: A Case Study in Generation of Program Transformation Systems. |
2000 |
210 |
Stratego is a domain specific language for the specification of program transformation systems. The design of Stratego is based on the paradigm of rewriting strategies: user-definable programs in a little language of strategy operators determine wher... |
| When Is A Type Refinement An Inductive Type? |
2011 |
195 |
Dependently typed programming languages allow sophisticated properties of data to be expressed within the type system. Of particular use in dependently typed programming are indexed types that refine data by computationally useful information. For ex... |