A delta for hybrid type checking

DOI10.1007/978-3-319-30936-1_22MaRDI QIDQ3188298zbMATH OpenOpenAlexFDO

Authors Peter J. Thiemann

Publication date 17 August 2016

Published in A List of Successes That Can Change the World (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-30936-1_22

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Recommendations

• Hybrid type checking
• Space-efficient gradual typing
• Shifting the blame. A blame calculus with delimited control
• Exploring the Design Space of Higher-Order Casts
• Threesomes, with and without blame

Cites work

• A syntactic approach to type soundness
• Contracts for higher-order functions
• Contracts made manifest
• Dynamic typing: Syntax and proof theory
• scientific article; zbMATH DE number 2163037 (Why is no real title available?)
• Optimizing synthesis with metasketches
• Secure distributed programming with value-dependent types
• Space-efficient gradual typing
• Subtyping dependent types
• Well-Typed Programs Can’t Be Blamed

Cited in

(2)

• Threesomes, with and without blame
• Hybrid type checking

Describes a project that uses

Uses Software

• Rosette
• F*

This page was built for publication: A delta for hybrid type checking

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