40 citations · 98 across the 22 of their papers we have counts for
24 papers
Programming Backpropagation with Reverse Handlers for Arrows
Takahiro Sanada, Keisuke Hoshino, Kenshin Hirai +1
We introduce a new programming language and its categorical semantics in order to design and implement neural networks within the framework of algebraic effects and handlers for ar…
Composing Codensity Bisimulations
Mayuko Kori, Kazuki Watanabe, Jurriaan Rot +1
Proving compositionality of behavioral equivalence on state-based systems with respect to algebraic operations is a classical and widely studied problem. We study a categorical for…
A Categorical Framework for Program Semantics and Semantic Abstraction
Shin-ya Katsumata, Xavier Rival, Jérémy Dubut
Categorical semantics of type theories are often characterized as structure-preserving functors. This is because in category theory both the syntax and the domain of interpretation…
Divergences on Monads for Relational Program Logics
Tetsuya Sato, Shin-ya Katsumata
Several relational program logics have been introduced for integrating reasoning about relational properties of programs and measurement of quantitative difference between computat…
The Lattice-Theoretic Essence of Property Directed Reachability Analysis
Mayuko Kori, Natsuki Urabe, Shin-ya Katsumata +2
We present LT-PDR, a lattice-theoretic generalization of Bradley's property directed reachability analysis (PDR) algorithm. LT-PDR identifies the essence of PDR to be an ingenious…
Robustifying Controller Specifications of Cyber-Physical Systems Against Perceptual Uncertainty
Tsutomu Kobayashi, Rick Salay, Ichiro Hasuo +3
Formal reasoning on the safety of controller systems interacting with plants is complex because developers need to specify behavior while taking into account perceptual uncertainty…
Architecture-Guided Test Resource Allocation Via Logic
Clovis Eberhart, Akihisa Yamada, Stefan Klikovits +4
We introduce a new logic named Quantitative Confidence Logic (QCL) that quantifies the level of confidence one has in the conclusion of a proof. By translating a fault tree represe…
Higher-order probabilistic adversarial computations: Categorical semantics and program logics
Alejandro Aguirre, Gilles Barthe, Marco Gaboardi +3
Adversarial computations are a widely studied class of computations where resource-bounded probabilistic adversaries have access to oracles, i.e., probabilistic procedures with pri…
Expressivity of Quantitative Modal Logics: Categorical Foundations via Codensity and Approximation
Yuichi Komorida, Shin-ya Katsumata, Clemens Kupke +2
A modal logic that is strong enough to fully characterize the behavior of a system is called expressive. Recently, with the growing diversity of systems to be reasoned about (proba…
Fibrational Initial Algebra-Final Coalgebra Coincidence over Initial Algebras: Turning Verification Witnesses Upside Down
Mayuko Kori, Ichiro Hasuo, Shin-ya Katsumata
The coincidence between initial algebras (IAs) and final coalgebras (FCs) is a phenomenon that underpins various important results in theoretical computer science. In this paper, w…
Control-Data Separation and Logical Condition Propagation for Efficient Inference on Probabilistic Programs
Ichiro Hasuo, Yuichiro Oyabu, Clovis Eberhart +3
We present a novel sampling framework for probabilistic programs. The framework combines two recent ideas -- \emph{control-data separation} and \emph{logical condition propagation}…
Graded Hoare Logic and its Categorical Semantics
Marco Gaboardi, Shin-ya Katsumata, Dominic Orchard +1
Deductive verification techniques based on program logics (i.e., the family of Floyd-Hoare logics) are a powerful approach for program reasoning. Recently, there has been a trend o…
Interaction laws of monads and comonads
Shin-ya Katsumata, Exequiel Rivas, Tarmo Uustalu
We introduce and study functor-functor and monad-comonad interaction laws as mathematical objects to describe interaction of effectful computations with behaviors of effect-perform…
Codensity Games for Bisimilarity
Yuichi Komorida, Shin-ya Katsumata, Nick Hu +2
Bisimilarity as an equivalence notion of systems has been central to process theory. Due to the recent rise of interest in quantitative systems (probabilistic, weighted, hybrid, et…
Differentiable Causal Computations via Delayed Trace
David Sprunger, Shin-ya Katsumata
We investigate causal computations taking sequences of inputs to sequences of outputs where the th output depends on the first inputs only. We model these in category theory…
Relational Differential Dynamic Logic
Juraj Kolčák, Ichiro Hasuo, Jérémy Dubut +3
In the field of quality assurance of hybrid systems (that combine continuous physical dynamics and discrete digital control), Platzer's differential dynamic logic (dL) is widely re…
A Coalgebraic View on Reachability
Thorsten Wißmann, Stefan Milius, Shin-ya Katsumata +1
Coalgebras for an endofunctor provide a category-theoretic framework for modeling a wide range of state-based systems of various types. We provide an iterative construction of the…
Path category for free - Open morphisms from coalgebras with non-deterministic branching
Thorsten Wißmann, Jérémy Dubut, Shin-ya Katsumata +1
There are different categorical approaches to variations of transition systems and their bisimulations. One is coalgebra for a functor G, where a bisimulation is defined as a span…
Codensity Lifting of Monads and its Dual
Shin-ya Katsumata, Tetsuya Sato, Tarmo Uustalu
We introduce a method to lift monads on the base category of a fibration to its total category. This method, which we call codensity lifting, is applicable to various fibrations wh…
Quantitative bisimulations using coreflections and open morphisms
Jérémy Dubut, Ichiro Hasuo, Shin-ya Katsumata +1
We investigate a canonical way of defining bisimilarity of systems when their semantics is given by a coreflection, typically in a category of transition systems. We use the fact,…
Probabilistic Relational Reasoning via Metrics
Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu +1
The Fuzz programming language [Reed and Pierce, 2010] uses an elegant linear type system combined with a monad-like type to express and reason about probabilistic sensitivity prope…
Approximate Span Liftings
Tetsuya Sato, Gilles Barthe, Marco Gaboardi +2
We develop new abstractions for reasoning about relaxations of differential privacy: Rényi differential privacy, zero-concentrated differential privacy, and truncated concentrated…
A Semantic Account of Metric Preservation
Arthur Azevedo de Amorim, Marco Gaboardi, Justin Hsu +2
Program sensitivity measures how robust a program is to small changes in its input, and is a fundamental notion in domains ranging from differential privacy to cyber-physical syste…
Extensional Models of Untyped Lambda-mu Calculus
Koji Nakazawa, Shin-ya Katsumata
This paper proposes new mathematical models of the untyped Lambda-mu calculus. One is called the stream model, which is an extension of the lambda model, in which each term is inte…