Cover Image

A Graded Modal Dependent Type Theory with Erasure, Formalized

Fuente: arXiv

Saved in:

Bibliographic Details
Main Authors:	Abel, Andreas, Danielsson, Nils Anders, Eriksson, Oskar
Format:	Preprint
Published:	2026
Subjects:	Logic in Computer Science Programming Languages
Online Access:	Acceder al recurso
Tags:	Add Tag No Tags, Be the first to tag this record!

Similar Items

Type Theory With Erasure
by: Theocharis, Constantine, et al.
Published: (2026)

DeLaM: A Dependent Layered Modal Type Theory for Meta-programming
by: Hu, Jason Z. S., et al.
Published: (2024)

Layered Modal Type Theories
by: Hu, Jason Z. S., et al.
Published: (2023)

Dependent Multiplicities in Dependent Linear Type Theory
by: Doré, Maximilian
Published: (2025)

Impredicativity in Linear Dependent Type Theory
by: Speight, Sam, et al.
Published: (2026)

Guard Analysis and Safe Erasure Gradual Typing: a Type System for Elixir
by: Castagna, Giuseppe, et al.
Published: (2024)

Foundations of Substructural Dependent Type Theory
by: Aberlé, C. B.
Published: (2024)

Dependent Type Refinements for Futures
by: Somayyajula, Siva, et al.
Published: (2023)

Compositional Program Verification with Polynomial Functors in Dependent Type Theory
by: Aberlé, C. B.
Published: (2026)

Towards Multiparty Session Types for Highly-Concurrent and Fault-Tolerant Web Applications
by: Casetta, Richard, et al.
Published: (2026)

WebPie: A Tiny Slice of Dependent Typing
by: Scholliers, Christophe
Published: (2024)

Pragmatics of Formally Verified Yet Efficient Static Analysis, in particular for Formally Verified Compilers
by: Monniaux, David
Published: (2024)

A Formally Verified Procedure for Width Inference in FIRRTL
by: Wang, Keyin, et al.
Published: (2026)

A Formal Semantics of the GraalVM Intermediate Representation
by: Webb, Brae J., et al.
Published: (2021)

Syntax and Semantics of Linear Dependent Types
by: Vákár, Matthijs
Published: (2014)

A Mixed Linear and Graded Logic: Proofs, Terms, and Models (with appendices)
by: Vollmer, Victoria, et al.
Published: (2024)

A Formalization of the Yul Language and Some Verified Yul Code Transformations
by: Coglio, Alessandro, et al.
Published: (2025)

Logical Relations for Formally Verified Authenticated Data Structures
by: Gregersen, Simon Oddershede, et al.
Published: (2025)

Formal Verification of a Token Sale Launchpad: A Compositional Approach in Dafny
by: Ukhanov, Evgeny
Published: (2025)

Formal Analysis of Networked PLC Controllers Interacting with Physical Environments
by: Lee, Jaeseo, et al.
Published: (2025)

Lax Modal Lambda Calculi
by: Valliappan, Nachiappan
Published: (2025)

Polynomial Universes in Homotopy Type Theory
by: Aberlé, C. B., et al.
Published: (2024)

From Semantics to Syntax: A Type Theory for Comprehension Categories
by: Najmaei, Niyousha, et al.
Published: (2025)

Orthologic Type Systems
by: Guilloud, Simon, et al.
Published: (2025)

Logic Programming with Extensible Types
by: Perez, Ivan, et al.
Published: (2026)

Type-Based Termination for Futures
by: Somayyajula, Siva, et al.
Published: (2021)

On the Expressivity of Typed Concurrent Calculi
by: Paulus, Joseph William Neal
Published: (2024)

Internalizing Representation Independence with Univalence
by: Angiuli, Carlo, et al.
Published: (2020)

On Representability of Multiple-Valued Functions by Linear Lambda Terms Typed with Second-order Polymorphic Type System
by: Matsuoka, Satoshi
Published: (2026)

Types, equations, dimensions and the Pi theorem
by: Botta, Nicola, et al.
Published: (2023)

Linear Contextual Metaprogramming and Session Types
by: Ângelo, Pedro, et al.
Published: (2024)

Typed compositional quantum computation with lenses
by: Garrigue, Jacques, et al.
Published: (2023)

A Type System for Data Flow and Alias Analysis in ReScript
by: Lund, Nicky Ask, et al.
Published: (2024)

Hybrid Intersection Types for PCF (Extended Version)
by: Barenbaum, Pablo, et al.
Published: (2024)

Monadic Intersection Types, Relationally (Extended Version)
by: Gavazzo, Francesco, et al.
Published: (2024)

Crash-Stop Failures in Asynchronous Multiparty Session Types
by: Barwell, Adam D., et al.
Published: (2023)

On Decidable and Undecidable Extensions of Simply Typed Lambda Calculus
by: Kobayashi, Naoki
Published: (2024)

Typed Non-determinism in Concurrent Calculi: The Eager Way
by: Heuvel, Bas van den, et al.
Published: (2024)

Resource-Bounded Type Theory: Compositional Cost Analysis via Graded Modalities
by: Mannucci, Mirco A., et al.
Published: (2025)

Reasoning about Weak Isolation Levels in Separation Logic
by: Mathiasen, Anders Alnor, et al.
Published: (2025)