Patricia Johann Ph.D

Dr. Johann is a full Professor in the Computer Science Department at Appalachian State University in Boone, NC, where she does research and teaches computer science courses. Before coming to Appalachian State University, she was a Reader (US equivalent: Professor) of Computer Science in the Mathematically Structured Programming group in the Department of Computer and Information Sciences at the University of Strathclyde in Glasgow, Scotland. Education: Ph.D. (Mathematics), Wesleyan University, 1991; B.A. (Mathematics), Reed College, 1985. For more biographical info & links to research visit: https://cs.appstate.edu/~johannp/

There are 40 included publications by Patricia Johann Ph.D:

TitleDateViewsBrief Description
Abstraction and Invariance for Algebraically Indexed Types 2013 386 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 748 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 1788 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 626 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 1437 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 1142 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 694 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 1927 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 1063 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 359 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 635 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 766 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 494 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 645 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 1647 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 1769 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 1194 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 104 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 250 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 1770 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 1357 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 2074 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 1614 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 861 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 422 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 686 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 1651 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 792 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 100 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 440 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 2410 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 1302 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 1502 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 1456 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 1010 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 473 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 432 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...