Parameterized cast calculi and reusable meta-theory for gradually typed lambda calculi
From MaRDI portal
Publication:5020907
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
- A Brief Overview of Agda – A Functional Language with Dependent Types
- Abstracting gradual typing
- Big types in little runtime: open-world soundness and collaborative blame for gradual type systems
- Blame and coercion: Together again for the first time
- Blame for all
- Calculating threesomes, with blame
- Consistent subtyping for all
- Dynamic typing: Syntax and proof theory
- Exploring the Design Space of Higher-Order Casts
- How to evaluate the performance of gradual type systems
- Hybrid type checking
- Isabelle/HOL. A proof assistant for higher-order logic
- Monotonic references for efficient gradual typing
- Operational semantics for multi-language programs
- Principal type schemes for gradual programs
- Space-efficient gradual typing
- The design and implementation of Typed Scheme
- Theorem Proving in Higher Order Logics
- Threesomes, with and without blame
- Well-Typed Programs Can’t Be Blamed
Describes a project that uses
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)
