Image de couverture de livre

Bounded First-Class Universe Levels in Dependent Type Theory

Fuente: arXiv

Enregistré dans:

Détails bibliographiques
Auteurs principaux:	Chan, Jonathan, Weirich, Stephanie
Format:	Preprint
Publié:	2025
Sujets:	Programming Languages Logic in Computer Science 03B38 (Primary) 68N15, 68V15 (Secondary) D.3.1; 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

Internalizing Extensions in Lattices of Type Theories
par: Chan, Jonathan
Publié: (2025)

Monoid Theory in Alonzo: A Little Theories Formalization in Simple Type Theory
par: Farmer, William M., et autres
Publié: (2023)

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)

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

The Solver's Paradox in Formal Problem Spaces
par: Rosko, Milan
Publié: (2025)

Formalizing Pick's Theorem in Isabelle/HOL
par: Binder, Sage, et autres
Publié: (2024)

Universal Algebra in UniMath
par: Amato, Gianluca, et autres
Publié: (2021)

Higher-Order Pattern Unification Modulo Similarity Relations
par: Dundua, Besik, et autres
Publié: (2025)

Algorithm and abstraction in formal mathematics
par: Macbeth, Heather
Publié: (2024)

An Alternative Approach to Formal Mathematics that Focuses on Communication and Accessibility
par: Farmer, William M.
Publié: (2026)

2-Coherent Internal Models of Homotopical Type Theory
par: Chen, Joshua
Publié: (2025)

A Logspace Constructive Proof of L=SL
par: Buss, Sam, et autres
Publié: (2025)

Psi-Turing Machines: Bounded Introspection for Complexity Barriers and Oracle Separations
par: Huseynzade, Rafig
Publié: (2025)

Proof complexity of universal algebra in a CSP dichotomy proof
par: Gaysin, Azza
Publié: (2024)

A Bisimulation-Invariance-Based Approach to the Separation of Polynomial Complexity Classes
par: Bruse, Florian, et autres
Publié: (2026)

Complete Robust Hybrid Systems Reachability
par: Wafa, Noah Abou El, et autres
Publié: (2026)

Arithmetics within the Linear Time Hierarchy
par: Pollett, Chris
Publié: (2025)

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

A classification of bisimilarities for general Markov decision processes
par: Moroni, Martín Santiago, et autres
Publié: (2024)

The complexity of bisimilarity on pointmass processes
par: Moroni, Martín Santiago, et autres
Publié: (2026)

A formalization of Borel determinacy in Lean
par: Manthe, Sven
Publié: (2025)

A Modular Lean 4 Framework for Confluence and Strong Normalization of Lambda Calculi with Products and Sums
par: Ramos, Arthur, et autres
Publié: (2025)

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

The Semantics of Metapropramming in Prolog
par: Warren, David S.
Publié: (2024)

Extended Nullstellensatz proof systems
par: Krajicek, Jan
Publié: (2023)

A proof complexity conjecture and the Incompleteness theorem
par: Krajicek, Jan
Publié: (2023)

A Lopez-Escobar Theorem for Continuous Domains
par: Bazhenov, Nikolay, et autres
Publié: (2023)

The Aurellion Function: A Recursive Fast-Growing Hierarchy Beyond Knuth Notation
par: Vodrazka, Daniel
Publié: (2025)

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

Truth-Aware Decoding: A Program-Logic Approach to Factual Language Generation
par: Alpay, Faruk, et autres
Publié: (2025)

Declarative distributed algorithms as axiomatic theories in three-valued modal logic over semitopologies
par: Gabbay, Murdoch J.
Publié: (2025)

The Tactician's Web of Large-Scale Formal Knowledge
par: Blaauwbroek, Lasse
Publié: (2024)

A Formalization of Abstract Rewriting in Agda
par: Arkle, Sam, et autres
Publié: (2026)

A Modular First Formalisation of Combinatorial Design Theory
par: Edmonds, Chelsea, et autres
Publié: (2021)

Deep Vision: A Formal Proof of Wolstenholmes Theorem in Lean 4
par: Linhares, Alexandre
Publié: (2026)

Formal P-Category Theory and Normalization by Evaluation in Rocq
par: Berry, David G., et autres
Publié: (2025)

A Qualitative Analysis of Kernel Extension for Higher Order Proof Checking
par: Wang, Shuai
Publié: (2024)

Verified Program Extraction in Number Theory: The Fundamental Theorem of Arithmetic and Relatives
par: Wiesnet, Franziskus
Publié: (2025)

An Expressive Trace Logic for Recursive Programs
par: Gurov, Dilian, et autres
Publié: (2024)