PaJAM generalizes JAM/IAM/PAM via backtracking depth and extracts its step count from non-idempotent intersection type derivations, yielding a polynomial reasonable cost model for bounded depth.
McDonell, Manuel M.T
3 Pith papers cite this work. Polarity classification is still indexing.
3
Pith papers citing it
verdicts
UNVERDICTED 3representative citing papers
CHAD is a homomorphic source-to-source transformation for forward- and reverse-mode AD on higher-order functional languages with arrays, proven correct via compositional logical relations.
CopilotVerifier generates bisimulation proofs via Crucible symbolic execution and What4 SMT to establish output equivalence and identical crash behavior between Copilot monitors and their compiled forms.
citing papers explorer
-
On Jumps, Interactions, and Intersection Types
PaJAM generalizes JAM/IAM/PAM via backtracking depth and extracts its step count from non-idempotent intersection type derivations, yielding a polynomial reasonable cost model for bounded depth.
-
CHAD: Combinatory Homomorphic Automatic Differentiation
CHAD is a homomorphic source-to-source transformation for forward- and reverse-mode AD on higher-order functional languages with arrays, proven correct via compositional logical relations.
-
Trustworthy Runtime Verification via Bisimulation (Extended Experience Report)
CopilotVerifier generates bisimulation proofs via Crucible symbolic execution and What4 SMT to establish output equivalence and identical crash behavior between Copilot monitors and their compiled forms.