Call-by-name gradual type theory

MaRDI QIDQ5214814zbMATH OpenFDO

Authors Max New, Daniel R. Licata

Publication date 5 February 2020

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

zbMATH Keywords

category theorydenotational semanticsgradual typingprogram logicstype systems

Mathematics Subject Classification ID

Logic in computer science (03B70) Categorical semantics of formal languages (18C50) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Recommendations

• Call-by-name gradual type theory
• Gradual type theory
• Abstracting gradual typing
• Monotonic references for efficient gradual typing
• Principal type schemes for gradual programs

Cites work

• A judgmental reconstruction of modal logic
• A theory of gradual effect systems
• A unified framework for generalized multicategories
• Abstracting gradual typing
• An effectful way to eliminate addiction to dependence
• Automatically generating the dynamic semantics of gradually typed languages
• Bifibrational functorial semantics of parametric polymorphism
• Call-by-name gradual type theory
• Contracts for higher-order functions
• Data Types as Lattices
• Dependent types and fibred computational effects
• Dynamic typing: Syntax and proof theory
• Fixed-point constructions in order-enriched categories
• Foundations of dependent interoperability
• Framed bicategories and monoidal fibrations
• Gradual refinement types
• scientific article; zbMATH DE number 3959364 (Why is no real title available?)
• scientific article; zbMATH DE number 177780 (Why is no real title available?)
• scientific article; zbMATH DE number 512792 (Why is no real title available?)
• scientific article; zbMATH DE number 1078585 (Why is no real title available?)
• scientific article; zbMATH DE number 195199 (Why is no real title available?)
• Notions of computation and monads
• Parametric Polymorphism through Run-Time Sealing or, Theorems for Low, Low Prices!
• Parametricity and local variables
• Relational properties of domains
• The Category-Theoretic Solution of Recursive Domain Equations
• The design and implementation of Typed Scheme
• Threesomes, with and without blame
• Well-Typed Programs Can’t Be Blamed

Cited in

(6)

• Call-by-name gradual type theory
• Gradual type theory
• Call-by-name gradual type theory
• Gradual Typing for Annotated Type Systems
• Galois connecting call-by-value and call-by-name
• Insights from univalent foundations: a case study using double categories

This page was built for publication: Call-by-name gradual type theory

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