Computer Science Department
School of Computer Science, Carnegie Mellon University
From Indexed Lax Logic to Intuitionistic Logic
Deepak Garg, Michael Carl Tschantz
We present translations from a logic with indexed lax modalities to first-order intuitionistic logic and intuitionistic linear logic. These translations rely on a continuation passing style encoding for the lax modalities. We show that our translations preserve provability of formulas.