6 papers
Polymorphic Metaprogramming with Memory Management -- An Adjoint Analysis of Metaprogramming
Junyoung Jang, Brigitte Pientka
We describe Elevator, a unifying polymorphic foundation for metaprogramming with memory management based on adjoint modalities. In this setting, we distinguish between multiple mem…
DeLaM: A Dependent Layered Modal Type Theory for Meta-programming
Jason Z. S. Hu, Brigitte Pientka
We scale layered modal type theory to dependent types, introducing DeLaM, dependent layered modal type theory. This type theory is novel in that we have one uniform type theory in…
SAT-DIFF: A Tree Diffing Framework Using SAT Solving
Chuqin Geng, Haolin Ye, Yihan Zhang +2
Computing differences between tree-structured data is a critical but challenging problem in software analysis. In this paper, we propose a novel tree diffing approach called SatDif…
Message-Observing Sessions
Ryan Kavanagh, Brigitte Pientka
We present Most, a process language with message-observing session types. Message-observing session types extend binary session types with type-level computation to specify communi…
Layered Modal Type Theories
Jason Z. S. Hu, Brigitte Pientka
We introduce layers to modal type theories, which subsequently enables type theories for pattern matching on code in meta-programming and clean and straightforward semantics.
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…