Typed Operational Semantics for Dependent Record Types
Yangyue Feng (Department of Computer Science, RHUL), Zhaohui Luo, (Department of Computer Science, RHUL)
TL;DR
This paper develops a typed operational semantics framework for a type system with dependent record types, establishing key meta-theoretic properties such as strong normalization, Church-Rosser, and subject reduction.
Contribution
It introduces a novel typed operational semantics approach for dependent record types and proves important meta-theoretic properties for this system.
Findings
Proves strong normalization for the dependent record type system
Establishes Church-Rosser property in the system
Demonstrates subject reduction holds in the system
Abstract
Typed operational semantics is a method developed by H. Goguen to prove meta-theoretic properties of type systems. This paper studies the metatheory of a type system with dependent record types, using the approach of typed operational semantics. In particular, the metatheoretical properties we have proved include strong normalisation, Church-Rosser and subject reduction.
Peer Reviews
No public reviews on file for this paper yet. If you reviewed it on a platform where reviews are public (OpenReview, ICLR, NeurIPS, ICML), you can paste yours below so the community can read it here.
Videos
No videos yet. Explain this paper in a talk, walkthrough, or lecture? Add one.