Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi

DOI10.1017/S0956796821000241OpenAlexW3211946171MaRDI QIDQ5020907

Tianyu Chen, Jeremy G. Siek

Publication date: 7 January 2022

Published in: Journal of Functional Programming (Search for Journal in Brave)

Full work available at URL: https://arxiv.org/abs/2001.11560

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Uses Software

• Coq
• Isabelle/HOL
• Agda
• PoplMark
• gradualizerDynamicSemantics
• Sage
• Flow

Cites Work

• Space-efficient gradual typing
• Dynamic typing: Syntax and proof theory
• Isabelle/HOL. A proof assistant for higher-order logic
• Consistent subtyping for all
• Monotonic References for Efficient Gradual Typing
• Principal Type Schemes for Gradual Programs
• Abstracting gradual typing
• A Brief Overview of Agda – A Functional Language with Dependent Types
• Operational semantics for multi-language programs
• The design and implementation of typed scheme
• Well-Typed Programs Can’t Be Blamed
• Exploring the Design Space of Higher-Order Casts
• How to evaluate the performance of gradual type systems
• Blame and coercion: Together again for the first time
• Calculating threesomes, with blame
• Threesomes, with and without blame
• Hybrid type checking
• Big types in little runtime: open-world soundness and collaborative blame for gradual type systems
• Blame for all
• Theorem Proving in Higher Order Logics

This page was built for publication: Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi