13 citations · 24 across the 11 of their papers we have counts for
12 papers
Phase Semantic Cut-elimination for Intuitionistic Linear Logic with Least and Greatest Fixed Points
Jun Suzuki, Charles Grellois, Katsuhiko Sano
This paper establishes the cut-elimination theorem for intuitionistic propositional multiplicative-additive linear logic with the least and greatest fixpoints (IMALL) by means o…
A coalgebraic higher-order modal fixed-point logic
Ryan Tay, Harsh Beohar, Charles Grellois
We introduce a coalgebraic extension of the higher-order modal fixed-point logic (HFL) which subsumes both HFL and its probabilistic extension. We show that the emptiness problem f…
Tree Automata Acceptance up to Measurable Defect
Anita Moyasari, Harsh Beohar, Charles Grellois +1
Automata acceptance can, in several situations of interest, be captured game-theoretically via acceptance games. The existence of a winning strategy for Verifier then captures the…
Adequate Losses via Quantitative Linear Logic
Matteo Capucci, Robert Atkey, Charles Grellois +2
As neural components are increasingly embedded in existing symbolic software -- including safety-critical systems -- the question arises of how to specify and enforce the safety of…
Intuitionistic Non-Normal Modal Logics: A general framework
Tiziano Dalmonte, Charles Grellois, Nicola Olivetti
We define a family of intuitionistic non-normal modal logics; they can bee seen as intuitionistic counterparts of classical ones. We first consider monomodal logics, which contain…
On the Termination Problem for Probabilistic Higher-Order Recursive Programs
Naoki Kobayashi, Ugo Dal Lago, Charles Grellois
In the last two decades, there has been much progress on model checking of both probabilistic systems and higher-order programs. In spite of the emergence of higher-order probabili…
Probabilistic Termination by Monadic Affine Sized Typing (Long Version)
Ugo Dal Lago, Charles Grellois
We introduce a system of monadic affine sized types, which substantially generalise usual sized types, and allows this way to capture probabilistic higher-order programs which term…
Indexed linear logic and higher-order model checking
Charles Grellois, Paul-André Melliès
In recent work, Kobayashi observed that the acceptance by an alternating tree automaton A of an infinite tree T generated by a higher-order recursion scheme G may be formulated as…
Finitary semantics of linear logic and higher-order model-checking
Charles Grellois, Paul-André Melliès
In this paper, we explain how the connection between higher-order model-checking and linear logic recently exhibited by the authors leads to a new and conceptually enlightening pro…
Relational semantics of linear logic and higher-order model-checking
Charles Grellois, Paul-André Melliès
In this article, we develop a new and somewhat unexpected connection between higher-order model-checking and linear logic. Our starting point is the observation that once embedded…
An infinitary model of linear logic
Charles Grellois, Paul-André Melliès
In this paper, we construct an infinitary variant of the relational model of linear logic, where the exponential modality is interpreted as the set of finite or countable multisets…
Algebraic theories, monads, and arities
Charles Grellois
Monads are of interest both in semantics and in higher dimensional algebra. It turns out that the idea behind usual notion finitary monads (whose values on all sets can be computed…