Image de couverture de livre

A Modular Lean 4 Framework for Confluence and Strong Normalization of Lambda Calculi with Products and Sums

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Ramos, Arthur, Oliveira, Anjolina, de Queiroz, Ruy, de Veras, Tiago
Format:	Preprint
Publié:	2025
Sujets:	Logic in Computer Science 03B70, 03B15, 68Q42 F.3.1; F.3.2; F.4.1
Accès en ligne:	Acceder al recurso
Tags:	Ajouter un tag Pas de tags, Soyez le premier à ajouter un tag!

Documents similaires

Thoughts on sub-Turing interactive computability
par: Japaridze, Giorgi
Publié: (2024)

Extracting total Amb programs from proofs
par: Berger, Ulrich, et autres
Publié: (2023)

Coalgebraic Satisfiability Checking for Arithmetic $μ$-Calculi
par: Hausmann, Daniel, et autres
Publié: (2022)

ProofCloud: A Proof Retrieval Engine for Verified Proofs in Higher Order Logic
par: Wang, Shuai
Publié: (2024)

Propositional Dynamic Logic has Craig Interpolation: a tableau-based proof
par: Borzechowski, Manfred, et autres
Publié: (2025)

Meaning as Use, Application, Employment, Purpose, Usefulness
par: de Queiroz, Ruy J. G. B.
Publié: (2025)

From the Notebooks to the Investigations and Beyond
par: de Queiroz, Ruy J. G. B.
Publié: (2025)

The logic of bunched implications is undecidable
par: Galatos, Nick, et autres
Publié: (2026)

The Orientation Boundary for Step-Duplicating Recursors: Mechanized Impossibility, Escape, and Certification
par: Rahnama, Moses
Publié: (2025)

Internal Effectful Forcing in System T
par: Escardo, Martin H., et autres
Publié: (2025)

Do not throw out the baby: Clarithmetics as alternatives to weak arithmetics
par: Japaridze, Giorgi
Publié: (2026)

A propositional cirquent calculus for computability logic
par: Japaridze, Giorgi
Publié: (2024)

Approximate Axiomatization for Differentially-Defined Functions
par: Platzer, André, et autres
Publié: (2025)

Node Replication: Theory And Practice
par: Kesner, Delia, et autres
Publié: (2022)

Gödel Mirror: A Formal System For Contradiction-Driven Recursion
par: Chan, Jhet
Publié: (2025)

Bennett's Conjecture in Lean 4: Counter-Models for the PSR-Reducibility of Spinoza's Propositions V and XIV
par: Nakamura, Yuki
Publié: (2026)

Univalent Material Set Theory
par: Gylterud, Håkon Robbestad, et autres
Publié: (2023)

Normal forms in cubical type theory
par: Huang, Xu
Publié: (2026)

Hereditary First-Order Logic: the tractable quantifier prefix classes
par: Bodirsky, Manuel, et autres
Publié: (2024)

On the Computational Power of Extensional ESO
par: Bodirsky, Manuel, et autres
Publié: (2025)

The Seifert-van Kampen Theorem via Computational Paths: A Formalized Approach to Computing Fundamental Groups
par: Ramos, Arthur F., et autres
Publié: (2025)

Continuous and algebraic domains in univalent foundations
par: de Jong, Tom, et autres
Publié: (2024)

Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory
par: Gylterud, Håkon Robbestad, et autres
Publié: (2020)

Two strong undefinability results in inquisitive and team semantics
par: Barbero, Fausto
Publié: (2024)

Weihrauch problems as containers
par: Pradic, Cécilia, et autres
Publié: (2025)

Formalizing Computational Paths and Fundamental Groups in Lean
par: Ramos, Arthur F., et autres
Publié: (2025)

Continuations and Completeness in Proof-theoretic Semantics
par: Gu, Tao, et autres
Publié: (2026)

A correspondence between the time and space complexity
par: Latkin, Ivan V.
Publié: (2023)

Nominal techniques as an Agda library
par: Gabbay, Murdoch J., et autres
Publié: (2026)

Support + Belief = Decision Trust
par: Aldini, Alessandro, et autres
Publié: (2024)

Formally Verifying a Transformation from MLTL Formulas to Regular Expressions
par: Wang, Zili, et autres
Publié: (2025)

Formalizing MLTL Formula Progression in Isabelle/HOL
par: Kosaian, Katherine, et autres
Publié: (2024)

Belief in Simplicial Complexes
par: Sink, Philip, et autres
Publié: (2025)

A Note on Proper Relational Structures
par: Bjorndahl, Adam, et autres
Publié: (2025)

Relational Connectors and Heterogeneous Bisimulations
par: Nora, Pedro, et autres
Publié: (2024)

On the expressive power of inquisitive epistemic logic
par: Ciardelli, Ivano, et autres
Publié: (2023)

Labelled Well Quasi Ordered Classes of Bounded Linear Clique-Width
par: Lopez, Aliaume
Publié: (2024)

Agent Interpolation for Knowledge
par: Bílková, Marta, et autres
Publié: (2025)

DHoTT: A Temporal Extension of Homotopy Type Theory for Semantic Drift
par: Poernomo, Iman
Publié: (2025)

ASP Chef grows Mustache to look better
par: Alviano, Mario, et autres
Publié: (2025)