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.

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

TitleDateViewsBrief Description
Abstraction and Invariance for Algebraically Indexed Types 2013 20 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 9 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 19 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 7 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 17 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 6 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 11 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 18 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 95 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 44 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 50 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 27 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 56 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 75 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 13 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 30 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 79 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 67 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 62 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 18 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 87 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 6 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 20 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 20 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 17 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 48 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...