Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi
From MaRDI portal
Publication:5020907
DOI10.1017/S0956796821000241OpenAlexW3211946171MaRDI QIDQ5020907FDOQ5020907
Authors: Jeremy G. Siek, Tianyu Chen 
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
Recommendations
- Publication:3478384
- scientific article; zbMATH DE number 4047683
- Realizing the dependently typed \(\lambda\)-calculus
- scientific article; zbMATH DE number 1342279
- The complexity of type inference for higher-order typed lambda calculi
- scientific article; zbMATH DE number 3902021
- scientific article; zbMATH DE number 1499090
- Formalization of metatheory of the Lambda Calculus in constructive type theory using the Barendregt variable convention
- Type checking and typability in domain-free lambda calculi
- Typed λ-calculus with recursive definitions
Cites Work
- Theorem Proving in Higher Order Logics
- Isabelle/HOL. A proof assistant for higher-order logic
- A Brief Overview of Agda – A Functional Language with Dependent Types
- Well-Typed Programs Can’t Be Blamed
- The design and implementation of Typed Scheme
- Dynamic typing: Syntax and proof theory
- Operational semantics for multi-language programs
- Exploring the Design Space of Higher-Order Casts
- Hybrid type checking
- Blame for all
- Space-efficient gradual typing
- Abstracting gradual typing
- Threesomes, with and without blame
- Consistent subtyping for all
- Monotonic references for efficient gradual typing
- Principal type schemes for gradual programs
- Blame and coercion: Together again for the first time
- How to evaluate the performance of gradual type systems
- Calculating threesomes, with blame
- Big types in little runtime: open-world soundness and collaborative blame for gradual type systems
Uses Software
This page was built for publication: Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5020907)
