Imagen de Portada

2-Coherent Internal Models of Homotopical Type Theory

Fuente: arXiv

Guardado en:

Detalles Bibliográficos
Autor principal:	Chen, Joshua
Formato:	Preprint
Publicado:	2025
Materias:	Logic in Computer Science Category Theory Logic 03B38, 03B70 (Primary) 18C50, 68Q55 (Secondary) F.4.1; F.3.2; D.3.1
Acceso en línea:	Acceder al recurso
Etiquetas:	Agregar Etiqueta Sin Etiquetas, Sea el primero en etiquetar este registro!

Ejemplares similares

Internal Effectful Forcing in System T
por: Escardo, Martin H., et al.
Publicado: (2025)

Continuous and algebraic domains in univalent foundations
por: de Jong, Tom, et al.
Publicado: (2024)

Formal P-Category Theory and Normalization by Evaluation in Rocq
por: Berry, David G., et al.
Publicado: (2025)

A Modular Lean 4 Framework for Confluence and Strong Normalization of Lambda Calculi with Products and Sums
por: Ramos, Arthur, et al.
Publicado: (2025)

A vector logic for extensional formal semantics
por: Quigley, Daniel
Publicado: (2024)

An Expressive Trace Logic for Recursive Programs
por: Gurov, Dilian, et al.
Publicado: (2024)

Terminal Coalgebras and Non-wellfounded Sets in Homotopy Type Theory
por: Gylterud, Håkon Robbestad, et al.
Publicado: (2020)

Matching logic -- a new axiomatization
por: Leuştean, Laurenţiu, et al.
Publicado: (2025)

Notes on applicative matching logic
por: Leuştean, Laurenţiu
Publicado: (2025)

A declarative approach to specifying distributed algorithms using three-valued modal logic
por: Gabbay, Murdoch J., et al.
Publicado: (2025)

Univalent Material Set Theory
por: Gylterud, Håkon Robbestad, et al.
Publicado: (2023)

Recursive Completion in Higher K-Models: Front-Seed Semantics, Proof-Relevant Witnesses, and the K-Infinity Model
por: Martinez-Rivillas, Daniel O., et al.
Publicado: (2026)

Continuations and Completeness in Proof-theoretic Semantics
por: Gu, Tao, et al.
Publicado: (2026)

Simply-typed constant-domain modal lambda calculus I: distanced beta reduction and combinatory logic
por: Walsh, Sean
Publicado: (2024)

Relational Connectors and Heterogeneous Bisimulations
por: Nora, Pedro, et al.
Publicado: (2024)

Braids, twists, trace and duality in combinatory algebras
por: Hasegawa, Masahito, et al.
Publicado: (2024)

The Solver's Paradox in Formal Problem Spaces
por: Rosko, Milan
Publicado: (2025)

On logical parameterizations and functional representability in local set theories
por: Hernández, Enrique Ruiz, et al.
Publicado: (2021)

Node Replication: Theory And Practice
por: Kesner, Delia, et al.
Publicado: (2022)

Encoding Argumentation Frameworks to Propositional Logic Systems
por: Tang, Shuai, et al.
Publicado: (2025)

Extracting total Amb programs from proofs
por: Berger, Ulrich, et al.
Publicado: (2023)

Projective Presentations of Lex Modalities
por: Williams, Mark Damuni
Publicado: (2025)

Nominal techniques as an Agda library
por: Gabbay, Murdoch J., et al.
Publicado: (2026)

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

Internalizing Extensions in Lattices of Type Theories
por: Chan, Jonathan
Publicado: (2025)

Propositional Dynamic Logic has Craig Interpolation: a tableau-based proof
por: Borzechowski, Manfred, et al.
Publicado: (2025)

Two-dimensional Kripke Semantics I: Presheaves
por: Kavvos, G. A.
Publicado: (2024)

A Coherence Construction for the Propositional Universe
por: Huang, Xu
Publicado: (2024)

A vector logic for intensional formal semantics
por: Quigley, Daniel
Publicado: (2026)

The Seifert-van Kampen Theorem via Computational Paths: A Formalized Approach to Computing Fundamental Groups
por: Ramos, Arthur F., et al.
Publicado: (2025)

Complete Robust Hybrid Systems Reachability
por: Wafa, Noah Abou El, et al.
Publicado: (2026)

Two-dimensional Kripke Semantics II: Stability and Completeness
por: Kavvos, G. A.
Publicado: (2024)

A Bisimulation-Invariance-Based Approach to the Separation of Polynomial Complexity Classes
por: Bruse, Florian, et al.
Publicado: (2026)

The logic of bunched implications is undecidable
por: Galatos, Nick, et al.
Publicado: (2026)

The biequivalence of path categories and axiomatic Martin-Löf type theories
por: Otten, Daniël, et al.
Publicado: (2025)

A correspondence between the time and space complexity
por: Latkin, Ivan V.
Publicado: (2023)

Bounded First-Class Universe Levels in Dependent Type Theory
por: Chan, Jonathan, et al.
Publicado: (2025)

Computing Distinguishing Formulae for Threshold-Based Behavioural Distances
por: Forster, Jonas, et al.
Publicado: (2026)

Remarks on Primitive Regulation
por: Rosko, Milan
Publicado: (2026)

Getting Wiser from Multiple Data: Probabilistic Updating according to Jeffrey and Pearl
por: Jacobs, Bart
Publicado: (2024)