Image de couverture de livre

S4 modal sequent calculus as intermediate logic and intermediate language

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Caspar, Jean, Munch-Maccagnoni, Guillaume
Format:	Preprint
Publié:	2026
Sujets:	Logic in Computer Science Programming Languages
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

Linear effects, exceptions, and resource safety: a Curry-Howard correspondence for destructors
par: Congard, Sidney, et autres
Publié: (2025)

Classical notions of computation and the Hasegawa-Thielecke theorem (extended version)
par: Mangel, Éléonore, et autres
Publié: (2025)

Tabular intermediate logics comparison
par: Rzążewski, Paweł, et autres
Publié: (2025)

Wiring the Pi-calculus to Denotational Semantics
par: Sakayori, Ken, et autres
Publié: (2026)

Proof systems for partial incorrectness logic (partial reverse Hoare logic)
par: Oda, Yukihiro
Publié: (2025)

Syntactically and semantically regular languages of lambda-terms coincide through logical relations
par: Moreau, Vincent, et autres
Publié: (2023)

A beginner guide to Iris, Coq and separation logic
par: Dietrich, Elizabeth
Publié: (2021)

A denotationally-based program logic for higher-order store
par: Aagaard, Frederik Lerbjerg, et autres
Publié: (2023)

Degree-preserving Godel logics with an involution: intermediate logics and (ideal) paraconsistency
par: Coniglio, M. E., et autres
Publié: (2026)

Compositional theories for host-core languages
par: Trotta, Davide, et autres
Publié: (2020)

A feasible and unitary quantum programming language
par: Díaz-Caro, Alejandro, et autres
Publié: (2023)

Guard Analysis and Safe Erasure Gradual Typing: a Type System for Elixir
par: Castagna, Giuseppe, et autres
Publié: (2024)

A programming language characterizing quantum polynomial time
par: Hainry, Emmanuel, et autres
Publié: (2022)

Extending Isabelle/HOL's Code Generator with support for the Go programming language
par: Stübinger, Terru, et autres
Publié: (2023)

Quantum modal logic
par: Tokuo, Kenji
Publié: (2025)

Interpolation for the two-way modal mu-calculus
par: Kloibhofer, Johannes, et autres
Publié: (2025)

Nested-sequent Calculus for Modal Logic MB
par: Kawano, Tomoaki
Publié: (2024)

Cut-elimination for the alternation-free modal mu-calculus
par: Afshari, Bahareh, et autres
Publié: (2025)

Making first order linear logic a generating grammar
par: Slavnov, Sergey
Publié: (2022)

Modal definability in Euclidean modal logics
par: Balbiani, Philippe, et autres
Publié: (2025)

Minimal modal logics, constructive modal logics and their relations
par: Dalmonte, Tiziano
Publié: (2023)

A programming language combining quantum and classical control
par: Dave, Kinnari, et autres
Publié: (2025)

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

Frex: dependently-typed algebraic simplification
par: Allais, Guillaume, et autres
Publié: (2023)

Intuitionistic monotone modal logic via translation
par: de Groot, Jim
Publié: (2025)

Intuitionistic modal logics: a minimal setting
par: Balbiani, Philippe, et autres
Publié: (2025)

Kleene algebra with commutativity conditions is undecidable
par: de Amorim, Arthur Azevedo, et autres
Publié: (2024)

Encoding call-by-push-value in the pi-calculus
par: Bennetzen, Benjamin, et autres
Publié: (2025)

Defining implication relation for classical logic
par: Fu, Li
Publié: (2013)

MiniF2F in Rocq: Automatic Translation Between Proof Assistants -- A Case Study
par: Viennot, Jules, et autres
Publié: (2025)

A formal specification of the jq language
par: Färber, Michael
Publié: (2024)

Intuitionistic modal logic LIK4 is decidable
par: Balbiani, Philippe, et autres
Publié: (2025)

On semantics of first-order justification logic with binding modalities
par: Yavorskaya, Tatiana, et autres
Publié: (2025)

Intrinsic and relative characterization results for logics with negative modalities
par: de Groot, Jim, et autres
Publié: (2025)

A dependently-typed calculus of event telicity and culminativity
par: Kovalev, Pavel, et autres
Publié: (2025)

Complexity of the Model Checking problem for inquisitive propositional and modal logic
par: Grilletti, Gianluca, et autres
Publié: (2024)

Complete and tractable machine-independent characterizations of second-order polytime
par: Hainry, Emmanuel, et autres
Publié: (2022)

Impredicativity in Linear Dependent Type Theory
par: Speight, Sam, et autres
Publié: (2026)

Foundations of Digital Circuits: Denotation, Operational, and Algebraic Semantics
par: Kaye, George
Publié: (2025)

CSLib: The Lean Computer Science Library
par: Barrett, Clark, et autres
Publié: (2026)