24 citations · 129 across the 22 of their papers we have counts for
29 papers
Adjoint Natural Deduction (Extended Version)
Junyoung Jang, Sophia Roshal, Frank Pfenning +1
Adjoint logic is a general approach to combining multiple logics with different structural properties, including linear, affine, strict, and (ordinary) intuitionistic logics, where…
A Saturation-Based Unification Algorithm for Higher-Order Rational Patterns
Zhibo Chen, Frank Pfenning
Higher-order unification has been shown to be undecidable. Miller discovered the pattern fragment and subsequently showed that higher-order pattern unification is decidable and has…
Dependent Type Refinements for Futures
Siva Somayyajula, Frank Pfenning
Type refinements combine the compositionality of typechecking with the expressivity of program logics, offering a synergistic approach to program verification. In this paper we app…
Parametric Subtyping for Structural Parametric Polymorphism
Henry DeYoung, Andreia Mordido, Frank Pfenning +1
We study the interaction of structural subtyping with parametric polymorphism and recursively defined type constructors. Although structural subtyping is undecidable in this settin…
Data Layout from a Type-Theoretic Perspective
Henry DeYoung, Frank Pfenning
The specifics of data layout can be important for the efficiency of functional programs and interaction with external libraries. In this paper, we develop a type-theoretic approach…
A Logical Framework with Higher-Order Rational (Circular) Terms
Zhibo Chen, Frank Pfenning
Logical frameworks provide natural and direct ways of specifying and reasoning within deductive systems. The logical framework LF and subsequent developments focus on finitary proo…