11 citations · 57 across the 11 of their papers we have counts for
13 papers
How Functorial Are (Deep) GADTs?
Patricia Johann, Pierre Cagne
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 t…
(Deep) Induction Rules for GADTs
Patricia Johann, Enrico Ghiorzi
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 extensio…
GADTs, Functoriality, Parametricity: Pick Two
Patricia Johann, Enrico Ghiorzi, Daniel Jeffries
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 m…
Parametricity for Nested Types and GADTs
Patricia Johann, Enrico Ghiorzi
This paper considers parametricity and its consequent free theorems for nested data types. Rather than representing nested types via their Church encodings in a higher-kinded or de…
On local presentability of T/A
Patricia Johann, Andrew Polonsky
We prove that if is a locally -presentable category and is a -accessible functor then is locally -presentab…
A General Framework for Relational Parametricity
Kristina Sojakova, Patricia Johann
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 Re…
Cubical Categories for Higher-Dimensional Parametricity
Patricia Johann, Kristina Sojakova
Reynolds' theory of relational parametricity formalizes parametric polymorphism for System F, thus capturing the idea that polymorphically typed System F programs always map relate…
A Productivity Checker for Logic Programming
E. Komendantskaya, P. Johann, M. Schmidt
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 lan…
Structural Resolution: a Framework for Coinductive Proof Search and Proof Construction in Horn Clause Logic
Ekaterina Komendantskaya, Patricia Johann, Martin Schmidt
Logic programming (LP) is a programming language based on first-order Horn clause logic that uses SLD-resolution as a semi-decision procedure. Finite SLD-computations are inductive…
Structural Resolution for Logic Programming
P. Johann, E. Komendantskaya, V. Komendantskiy
We introduce a Three Tier Tree Calculus (3TC) that defines in a systematic way three tiers of tree structures underlying proof search in logic programming. We use 3TC to define a n…
Indexed Induction and Coinduction, Fibrationally
Neil Ghani, Patricia Johann, Clement Fumex
This paper extends the fibrational approach to induction and coinduction pioneered by Hermida and Jacobs, and developed by the current authors, in two key directions. First, we pre…
Generic Fibrational Induction
Neil Ghani, Patricia Johann, Clement Fumex
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 res…
Refining Inductive Types
Robert Atkey, Patricia Johann, Neil Ghani
Dependently typed programming languages allow sophisticated properties of data to be expressed within the type system. Of particular use in dependently typed programming are indexe…