| Abstraction and Invariance for Algebraically Indexed Types |
2013 |
384 |
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 |
517 |
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 Combinatory Logic Approach To Higher-order E-unification |
1995 |
741 |
Let E be a first-order equational theory. A translation of typed higher-order E-unification problems into a typed combinatory logic framework is presented and justified. The case in which E admits presentation as a convergent term rewriting system is... |
| Deep Induction: Induction Rules For (Truly) Nested Types |
2020 |
1769 |
This paper introduces deep induction, and shows that it is the notion of induction most appropriate to nested types and other data types defined over, or mutually recursively with, (other) such types. Standard induction rules induct over only the top... |
| (Deep) Induction Rules For GADTs |
2022 |
613 |
Deep data types are those that are constructed from other data types, including, possibly, themselves. In this case, they are said to be truly nested. Deep induction is an extension of structural induction that traverses all of the structure in a dee... |
| A Family Of Syntactic Logical Relations For The Semantics Of Haskell-Like Languages |
2009 |
1428 |
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 |
1133 |
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 |
689 |
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 |
1912 |
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... |
| Free Theorems In The Presence Of seq |
2004 |
1041 |
Parametric polymorphism constrains the behavior of pure functional programs in a way that allows the derivation of interesting theorems about them solely from their types, i.e., virtually for free. Unfortunately, the standard parametricity theorem fa... |
| Fusing Logic And Control With Local Transformations: An Example Optimization |
2001 |
353 |
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... |
| GADTs, Functoriality, Parametricity: Pick Two |
2021 |
628 |
GADTs can be represented either as their Church encodings a la Atkey, or as fixpoints a la Johann and Polonsky. While a GADT represented as its Church encoding need not support a map function satisfying the functor laws, the fixpoint representation o... |
| A General Framework For Relational Parametricity |
2018 |
760 |
Reynolds’ original theory of relational parametricity was intended to capture the idea that polymorphically typed System F programs preserve all relations between inputs. But as Reynolds himself later showed, his theory can only be formalized in a me... |
| A Generalization of Short-Cut Fusion and Its Correctness Proof |
2002 |
490 |
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 |
642 |
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 |
1636 |
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 |
1764 |
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... |
| Higher-Kinded Data Types: Syntax And Semantics |
2019 |
1171 |
We present a grammar for a robust class of data types that includes algebraic data types (ADTs), (truly) nested types, generalized algebraic data types (GADTs), and their higher-kinded analogues. All of the data types our grammar defines, as well as ... |
| How Functorial Are (Deep) GADTs? |
2022 |
103 |
It is well-known that GADTs do not admit standard map functions of the kind supported by ADTs and nested types. In addition, standard map functions are insufficient to distribute their data-changing argument functions over all of the structure presen... |
| The Impact Of seq On Free Theorems-Based Program Transformations |
2006 |
249 |
Parametric polymorphism constrains the behavior of pure functional programs in a way that allows the derivation of interesting theorems about them solely from their types, i.e., virtually for free. Unfortunately, standard parametricity results — incl... |
| An Improved General E-unification Method |
1992 |
1757 |
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 |
1348 |
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... |
| Initial Algebra Semantics Is Enough! |
2007 |
2020 |
Initial algebra semantics is a cornerstone of the theory of modern functional programming languages. For each inductive data type, it provides a fold combinator encapsulating structured recursion over data of that type, a Church encoding, a build com... |
| Interleaving Data and Effects |
2015 |
1606 |
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 ... |
| Local Presentability Of Certain Comma Categories |
2019 |
851 |
It follows from standard results that if A and C are locally ^presentable categories and F:A^C is a ^-accessible functor, then the comma category IdC^F is locally ^-presentable. We show that, under the same hypotheses, F^IdC is also locally ^-present... |
| Monadic Augment And Generalized Short Cut Fusion |
2007 |
416 |
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 |
682 |
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 |
1639 |
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... |
| Parametricity For Primitive Nested Types |
2021 |
784 |
This paper considers parametricity and its resulting free theorems for nested data types. Rather than representing nested types via their Church encodings in a higher-kinded or dependently typed extension of System F, we adopt a functional programmin... |
| A Productivity Checker For Logic Programming |
2016 |
99 |
Automated analysis of recursive derivations in logic programming is known to be a hard problem. Both termination and non-termination are undecidable problems in Turing-complete languages. However, some declarative languages offer a practical work-aro... |
| Refining Inductive Types |
2012 |
434 |
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 |
2393 |
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 |
1292 |
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 |
1496 |
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 |
1449 |
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... |
| Staged Notational Definitions |
2003 |
996 |
Recent work proposed defining type-safe macros via interpretation into a multi-stage language. The utility of this approach was illustrated with a language called MacroML, in which all type checking is carried out before macro expansion. Building on ... |
| Structural Resolution for Automated Verification |
2015 |
359 |
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 |
359 |
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 |
468 |
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 |
431 |
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... |