Cover Image

S4 modal sequent calculus as intermediate logic and intermediate language

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Caspar, Jean, Munch-Maccagnoni, Guillaume
Format:	Preprint
Published:	2026
Subjects:	Logic in Computer Science Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Linear effects, exceptions, and resource safety: a Curry-Howard correspondence for destructors
by: Congard, Sidney, et al.
Published: (2025)

Classical notions of computation and the Hasegawa-Thielecke theorem (extended version)
by: Mangel, Éléonore, et al.
Published: (2025)

Tabular intermediate logics comparison
by: Rzążewski, Paweł, et al.
Published: (2025)

Wiring the Pi-calculus to Denotational Semantics
by: Sakayori, Ken, et al.
Published: (2026)

Proof systems for partial incorrectness logic (partial reverse Hoare logic)
by: Oda, Yukihiro
Published: (2025)

Syntactically and semantically regular languages of lambda-terms coincide through logical relations
by: Moreau, Vincent, et al.
Published: (2023)

A beginner guide to Iris, Coq and separation logic
by: Dietrich, Elizabeth
Published: (2021)

A denotationally-based program logic for higher-order store
by: Aagaard, Frederik Lerbjerg, et al.
Published: (2023)

Degree-preserving Godel logics with an involution: intermediate logics and (ideal) paraconsistency
by: Coniglio, M. E., et al.
Published: (2026)

Compositional theories for host-core languages
by: Trotta, Davide, et al.
Published: (2020)

A feasible and unitary quantum programming language
by: Díaz-Caro, Alejandro, et al.
Published: (2023)

Guard Analysis and Safe Erasure Gradual Typing: a Type System for Elixir
by: Castagna, Giuseppe, et al.
Published: (2024)

A programming language characterizing quantum polynomial time
by: Hainry, Emmanuel, et al.
Published: (2022)

Extending Isabelle/HOL's Code Generator with support for the Go programming language
by: Stübinger, Terru, et al.
Published: (2023)

Quantum modal logic
by: Tokuo, Kenji
Published: (2025)

Interpolation for the two-way modal mu-calculus
by: Kloibhofer, Johannes, et al.
Published: (2025)

Nested-sequent Calculus for Modal Logic MB
by: Kawano, Tomoaki
Published: (2024)

Cut-elimination for the alternation-free modal mu-calculus
by: Afshari, Bahareh, et al.
Published: (2025)

Making first order linear logic a generating grammar
by: Slavnov, Sergey
Published: (2022)

Modal definability in Euclidean modal logics
by: Balbiani, Philippe, et al.
Published: (2025)

Minimal modal logics, constructive modal logics and their relations
by: Dalmonte, Tiziano
Published: (2023)

A programming language combining quantum and classical control
by: Dave, Kinnari, et al.
Published: (2025)

A Comprehensive Survey of the Lean 4 Theorem Prover: Architecture, Applications, and Advances
by: Tang, Xichen
Published: (2025)

Frex: dependently-typed algebraic simplification
by: Allais, Guillaume, et al.
Published: (2023)

Intuitionistic monotone modal logic via translation
by: de Groot, Jim
Published: (2025)

Intuitionistic modal logics: a minimal setting
by: Balbiani, Philippe, et al.
Published: (2025)

Kleene algebra with commutativity conditions is undecidable
by: de Amorim, Arthur Azevedo, et al.
Published: (2024)

Encoding call-by-push-value in the pi-calculus
by: Bennetzen, Benjamin, et al.
Published: (2025)

Defining implication relation for classical logic
by: Fu, Li
Published: (2013)

MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study
by: Viennot, Jules, et al.
Published: (2025)

A formal specification of the jq language
by: Färber, Michael
Published: (2024)

Intuitionistic modal logic LIK4 is decidable
by: Balbiani, Philippe, et al.
Published: (2025)

On semantics of first-order justification logic with binding modalities
by: Yavorskaya, Tatiana, et al.
Published: (2025)

Intrinsic and relative characterization results for logics with negative modalities
by: de Groot, Jim, et al.
Published: (2025)

A dependently-typed calculus of event telicity and culminativity
by: Kovalev, Pavel, et al.
Published: (2025)

Complexity of the Model Checking problem for inquisitive propositional and modal logic
by: Grilletti, Gianluca, et al.
Published: (2024)

Complete and tractable machine-independent characterizations of second-order polytime
by: Hainry, Emmanuel, et al.
Published: (2022)

Impredicativity in Linear Dependent Type Theory
by: Speight, Sam, et al.
Published: (2026)

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
by: Kaye, George
Published: (2025)

CSLib: The Lean Computer Science Library
by: Barrett, Clark, et al.
Published: (2026)