Subtyping without reduction

DOI10.1007/978-3-031-16912-0_2OpenAlexW4296963692MaRDI QIDQ6109205

Brandon Hewer, G. Hutton

Publication date: 30 June 2023

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-031-16912-0_2

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Cites Work

• Induction-recursion and initial algebras.
• Pattern matching without K
• Cubical Type Theory: a constructive interpretation of the univalence axiom
• Cubical Agda: A dependently typed programming language with univalence and higher inductive types
• Small Induction Recursion
• Indexed containers
• Homotopy Type Theory: Univalent Foundations of Mathematics