Buchumschlag

Formal P-Category Theory and Normalization by Evaluation in Rocq

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Berry, David G., Fiore, Marcelo P.
Format:	Preprint
Veröffentlicht:	2025
Schlagworte:	Logic in Computer Science Category Theory 03B40, 03B38, 68N18 F.3.2; F.4.1
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

Internal Effectful Forcing in System T
von: Escardo, Martin H., et al.
Veröffentlicht: (2025)

2-Coherent Internal Models of Homotopical Type Theory
von: Chen, Joshua
Veröffentlicht: (2025)

Continuous and algebraic domains in univalent foundations
von: de Jong, Tom, et al.
Veröffentlicht: (2024)

A vector logic for extensional formal semantics
von: Quigley, Daniel
Veröffentlicht: (2024)

Projective Presentations of Lex Modalities
von: Williams, Mark Damuni
Veröffentlicht: (2025)

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

Simply-typed constant-domain modal lambda calculus I: distanced beta reduction and combinatory logic
von: Walsh, Sean
Veröffentlicht: (2024)

Kripke-Joyal forcing for type theory and uniform fibrations
von: Awodey, S., et al.
Veröffentlicht: (2021)

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

Univalent Material Set Theory
von: Gylterud, Håkon Robbestad, et al.
Veröffentlicht: (2023)

A Coherence Construction for the Propositional Universe
von: Huang, Xu
Veröffentlicht: (2024)

Simplicial Homotopy Type Theory is not just Simplicial: What are $\infty$-Categories?
von: Rasekh, Nima
Veröffentlicht: (2025)

Meaning as Use, Application, Employment, Purpose, Usefulness
von: de Queiroz, Ruy J. G. B.
Veröffentlicht: (2025)

From the Notebooks to the Investigations and Beyond
von: de Queiroz, Ruy J. G. B.
Veröffentlicht: (2025)

The Tactician's Web of Large-Scale Formal Knowledge
von: Blaauwbroek, Lasse
Veröffentlicht: (2024)

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

The Frobenius equivalence and Beck-Chevalley condition for Algebraic Weak Factorisation Systems
von: van Woerkom, Wijnand, et al.
Veröffentlicht: (2024)

Continuations and Completeness in Proof-theoretic Semantics
von: Gu, Tao, et al.
Veröffentlicht: (2026)

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

Monoid Theory in Alonzo: A Little Theories Formalization in Simple Type Theory
von: Farmer, William M., et al.
Veröffentlicht: (2023)

Type Theory with Explicit Universe Polymorphism (revised and extended version)
von: Bezem, Marc, et al.
Veröffentlicht: (2022)

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

Non-Standard Models of Homotopy Type Theory
von: Rasekh, Nima
Veröffentlicht: (2025)

A vector logic for intensional formal semantics
von: Quigley, Daniel
Veröffentlicht: (2026)

Y is a least fixed point combinator
von: Helfer, Joseph
Veröffentlicht: (2025)

Monoidal closure of Grothendieck constructions via $Σ$-tractable monoidal structures and Dialectica formulas
von: Nunes, Fernando Lucatelli, et al.
Veröffentlicht: (2024)

Substructural fixed-point theorems and the diagonal argument: theme and variations
von: Roberts, David Michael
Veröffentlicht: (2021)

The Orientation Boundary for Step-Duplicating Recursors: Mechanized Impossibility, Escape, and Certification
von: Rahnama, Moses
Veröffentlicht: (2025)

Beyond Eckmann-Hilton: Commutativity in Higher Categories
von: Benjamin, Thibaut, et al.
Veröffentlicht: (2025)

On logical parameterizations and functional representability in local set theories
von: Hernández, Enrique Ruiz, et al.
Veröffentlicht: (2021)

Arrow algebras
von: Berg, Benno van den, et al.
Veröffentlicht: (2023)

Gödel coding on fibrations and geminal categories
von: Ikeda, Yuto
Veröffentlicht: (2026)

A 2-categorical approach to the semantics of dependent type theory with computation axioms
von: Spadetto, Matteo
Veröffentlicht: (2025)

Generalized Chevalley criteria in simplicial homotopy type theory
von: Weinberger, Jonathan
Veröffentlicht: (2024)

Two-sided cartesian fibrations of synthetic $(\infty,1)$-categories
von: Weinberger, Jonathan
Veröffentlicht: (2022)

A Classifying Topos for the Spectrum of Equivalences
von: Oggad, Kenan
Veröffentlicht: (2026)

Internal sums for synthetic fibered $(\infty,1)$-categories
von: Weinberger, Jonathan
Veröffentlicht: (2022)

A New Overture to Classical Simple Type Theory, Ketonen-type Gentzen and Tableau Systems
von: Miwa, Tadayoshi, et al.
Veröffentlicht: (2026)

Remarks on Primitive Regulation
von: Rosko, Milan
Veröffentlicht: (2026)

Smooth and Proper Maps
von: Anel, Mathieu, et al.
Veröffentlicht: (2024)