13 citations · 24 across the 11 of their papers we have counts for
9 papers · 1 filter
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…
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…