3 papers
cs.PL2026
Multicategorical Semantics for Untyped Effects
Ariel Grunfeld, Liron Cohen
Completeness proofs in categorical semantics usually proceed by building a syntactic category whose composition is given by substitution. For untyped effectful Call-by-Value langua…
cs.LO2025
Syntactic Effectful Realizability in Higher-Order Logic
Liron Cohen, Ariel Grunfeld, Dominik Kirst +1
Realizability interprets propositions as specifications for computational entities in programming languages. Specifically, syntactic realizability is a powerful machinery that hand…
cs.LO2025
From Partial to Monadic: Combinatory Algebra with Effects
Liron Cohen, Ariel Grunfeld, Dominik Kirst +1
Partial Combinatory Algebras (PCAs) provide a foundational model of the untyped -calculus and serve as the basis for many notions of computability, such as realizability theory…