4 papers
The Duality of Information Flow: Reconciling Robust Downgrading with Non-Interference
Hemant Gouni, Frank Pfenning, Jonathan Aldrich
Non-interference properties, spanning confidentiality and integrity, have long enjoyed a position as the high water mark of program security guarantees. Information flow type syste…
Ordered Adjoint Logic
Sophia Roshal, Frank Pfenning
Ordered logics and type systems have been used in a variety of applications including computational linguistics, memory allocation, stream processing, logical frameworks, parametri…
CoLF Logic Programming as Infinitary Proof Exploration
Zhibo Chen, Frank Pfenning
Logical Frameworks such as Automath [de Bruijn, 1968] or LF [Harper et al., 1993] were originally conceived as metalanguages for the specification of foundationally uncommitted ded…
Substructural Parametricity
C. B. Aberlé, Chris Martens, Frank Pfenning
Ordered, linear, and other substructural type systems allow us to expose deep properties of programs at the syntactic level of types. In this paper, we develop a family of unary lo…