Gradual type theory

DOI10.1017/S0956796821000125MaRDI QIDQ5019016zbMATH OpenOpenAlexFDO

Authors Max New, Daniel R. Licata, Amal Ahmed

Publication date 27 December 2021

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

Copyright license Creative Commons Attribution 4.0 International

Full work available at URL https://doi.org/10.1017/s0956796821000125

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18)

Recommendations

• Call-by-name gradual type theory
• Call-by-name gradual type theory
• Abstracting gradual typing
• Space-efficient gradual typing
• Big types in little runtime: open-world soundness and collaborative blame for gradual type systems

Cites work

• scientific article; zbMATH DE number 1330443 (Why is no real title available?)
• scientific article; zbMATH DE number 2120508 (Why is no real title available?)
• scientific article; zbMATH DE number 7350775 (Why is no real title available?)
• Abstracting gradual typing
• An effect system for algebraic effects and handlers
• Automatically generating the dynamic semantics of gradually typed languages
• Big types in little runtime: open-world soundness and collaborative blame for gradual type systems
• Call-by-name gradual type theory
• Call-by-name gradual type theory
• Contextual isomorphisms
• Contracts for higher-order functions
• Contracts made manifest
• Dependent types and fibred computational effects
• Do be do be do
• Dynamic typing: Syntax and proof theory
• Exploring the Design Space of Higher-Order Casts
• Foundations of dependent interoperability
• Gradual type theory
• How to evaluate the performance of gradual type systems
• Locus solum: From the rules of logic to the logic of rules.
• Models of a non-associative composition
• Notions of computation and monads
• Operational reasoning for functions with local state
• Polarized Substructural Session Types
• Programming Languages and Systems
• Space-efficient gradual typing
• Space-efficient manifest contracts
• Static contract checking for Haskell
• The Gradualizer: a methodology and algorithm for generating gradual type systems
• The design and implementation of Typed Scheme
• The interaction of contracts and laziness
• The recursive union of some gradual types
• Threesomes, with and without blame
• Typed Contracts for Functional Programming
• Well-Typed Programs Can’t Be Blamed

Cited in

(28)

• Galois connecting call-by-value and call-by-name
• The Gradualizer: a methodology and algorithm for generating gradual type systems
• Gradual program verification
• How to evaluate the performance of gradual type systems
• Well-Typed Programs Can’t Be Blamed
• Gradual ownership types
• The recursive union of some gradual types
• Principal type schemes for gradual programs
• Consistent subtyping for all
• Gradual refinement types
• Sums of uncertainty: refinements go gradual
• Exploring the Design Space of Higher-Order Casts
• Dynamic typing: Syntax and proof theory
• Call-by-name gradual type theory
• Abstracting gradual typing
• Pragmatic gradual polymorphism with references
• A gradual interpretation of union types
• Call-by-name gradual type theory
• Gradual System F
• Monotonic references for efficient gradual typing
• Big types in little runtime: open-world soundness and collaborative blame for gradual type systems
• Space-efficient gradual typing
• Gradual typing embedded securely in JavaScript
• Gradual Typing for Annotated Type Systems
• Reconciling noninterference and gradual typing
• Type Inference for Rank 2 Gradual Intersection Types
• Automatically generating the dynamic semantics of gradually typed languages
• Gradual type theory

This page was built for publication: Gradual type theory

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5019016)