Buchumschlag

Definitional Functoriality for Dependent (Sub)Types -- Extended version

Fuente: arXiv

Gespeichert in:

Bibliographische Detailangaben
Hauptverfasser:	Laurent, Théo, Lennon-Bertrand, Meven, Maillard, Kenji
Format:	Preprint
Veröffentlicht:	2023
Schlagworte:	Programming Languages Logic in Computer Science D.3.1; F.3.2; F.3; F.4.1
Online-Zugang:	Acceder al recurso
Tags:	Tag hinzufügen Keine Tags, Fügen Sie den ersten Tag hinzu!

Ähnliche Einträge

AdapTT: Functoriality for Dependent Type Casts
von: Adjedj, Arthur, et al.
Veröffentlicht: (2025)

What does it take to certify a conversion checker?
von: Lennon-Bertrand, Meven
Veröffentlicht: (2025)

Genericity Through Stratification
von: Arrial, Victor, et al.
Veröffentlicht: (2024)

Separation Logic of Generic Resources via Sheafeology
von: van Starkenburg, Berend, et al.
Veröffentlicht: (2025)

Infinitary Refinement Types for Temporal Properties in Scott Domains
von: Riba, Colin, et al.
Veröffentlicht: (2025)

Generically Automating Separation Logic by Functors, Homomorphisms and Modules
von: Xu, Qiyuan, et al.
Veröffentlicht: (2024)

Bidirectional Interpolation for the Lambda-Calculus -- Revisiting and Formalising Craig-Čubrić Interpolation
von: Bertrand, Meven Lennon, et al.
Veröffentlicht: (2026)

Compile-Time Tensor Shape Checking via Staged Shape-Dependent Types
von: Suwa, Takashi, et al.
Veröffentlicht: (2026)

Explicit Weakening
von: Wadler, Philip
Veröffentlicht: (2024)

Extending the Quantitative Pattern-Matching Paradigm
von: Alves, Sandra, et al.
Veröffentlicht: (2024)

Simple Types for Polymorphic Functions
von: Jay, Barry, et al.
Veröffentlicht: (2026)

Verified VCG and Verified Compiler for Dafny
von: Nezamabadi, Daniel, et al.
Veröffentlicht: (2025)

LeanLTL: A unifying framework for linear temporal logics in Lean
von: Vin, Eric, et al.
Veröffentlicht: (2025)

Unified Fairness for Weak Memory Verification
von: Abdulla, Parosh Aziz, et al.
Veröffentlicht: (2023)

Node Replication: Theory And Practice
von: Kesner, Delia, et al.
Veröffentlicht: (2022)

Intersection Types for a Computational Lambda-Calculus with Global State
von: de'Liguoro, Ugo, et al.
Veröffentlicht: (2021)

Stratified Type Theory
von: Chan, Jonathan, et al.
Veröffentlicht: (2023)

A Graded Modal Type Theory for Pulse Schedules
von: Adams, Robin, et al.
Veröffentlicht: (2025)

Closure Conversion, Flat Environments, and the Complexity of Abstract Machines
von: Accattoli, Beniamino, et al.
Veröffentlicht: (2025)

Verifying Tree-Manipulating Programs via CHCs
von: Faella, Marco, et al.
Veröffentlicht: (2025)

Gradual Guarantee via Step-Indexed Logical Relations in Agda
von: Siek, Jeremy G.
Veröffentlicht: (2024)

The Lambda Calculus is Quantifiable
von: Maestracci, Valentin, et al.
Veröffentlicht: (2024)

TensorRight: Automated Verification of Tensor Graph Rewrites
von: Arora, Jai, et al.
Veröffentlicht: (2025)

Nominal Algebraic-Coalgebraic Data Types, with Applications to Infinitary Lambda-Calculi
von: Cerda, Rémy
Veröffentlicht: (2025)

Modelling Recursion and Probabilistic Choice in Guarded Type Theory
von: Stassen, Philipp Jan Andries, et al.
Veröffentlicht: (2024)

BinSub: The Simple Essence of Polymorphic Type Inference for Machine Code
von: Smith, Ian
Veröffentlicht: (2024)

The Denotational Semantics of SSA
von: Ghalayini, Jad Elkhaleq, et al.
Veröffentlicht: (2024)

Abstract clones for abstract syntax
von: Arkor, Nathanael, et al.
Veröffentlicht: (2021)

The Relational Machine Calculus
von: Barrett, Chris, et al.
Veröffentlicht: (2024)

Qurts: Automatic Quantum Uncomputation by Affine Types with Lifetime
von: Hirata, Kengo, et al.
Veröffentlicht: (2024)

On Modular Termination Proofs of General Logic Programs
von: Bossi, Annalisa, et al.
Veröffentlicht: (2000)

Sequence-Based Abstract Interpretation of Prolog
von: Charlier, Baudouin Le, et al.
Veröffentlicht: (2000)

Conformance Games for Graded Semantics
von: Forster, Jonas, et al.
Veröffentlicht: (2024)

Modelling Distributed Applications with Mixed-Choice Stateful Typestates
von: Parrinha, Francisco, et al.
Veröffentlicht: (2026)

A Type Theory for Probabilistic and Bayesian Reasoning
von: Adams, Robin, et al.
Veröffentlicht: (2015)

Interpreting De Finetti's theorem in the Category of Integrable Cones (long version)
von: Raphaëlle, Crubillé
Veröffentlicht: (2026)

Automating the Derivation of Unification Algorithms: A Case Study in Deductive Program Synthesis
von: Waldinger, Richard
Veröffentlicht: (2025)

Refactoring-as-Propositions: Proved Refactoring of Hybrid Systems via Proved Refinements
von: Prebet, Enguerrand, et al.
Veröffentlicht: (2026)

Uniform Substitution for Differential Refinement Logic
von: Prebet, Enguerrand, et al.
Veröffentlicht: (2024)

Forall-Exists Relational Verification by Filtering to Forall-Forall
von: Nagasamudram, Ramana, et al.
Veröffentlicht: (2025)