Semantic subtyping with an SMT solver

DOI10.1017/S0956796812000032MaRDI QIDQ2913944zbMATH OpenOpenAlexFDO

Authors Gavin M. Bierman, Andrew D. Gordon, Cătălin Hriţcu, David Langworthy

Publication date 21 September 2012

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

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

zbMATH Keywords

first-order functional language

Mathematics Subject Classification ID

Theory of programming languages (68N15) Functional programming and lambda calculus (68N18)

Recommendations

• Semantic subtyping with an SMT solver
• Nested refinements: a logic for duck typing
• Semantic subtyping, dealing set-theoretically with function, union, intersection, and negation types
• Refinement types for Haskell
• Automata, Languages and Programming

Cites work

• A syntactic approach to type soundness
• Deciding validity in a spatial logic for trees
• Dependent types with subtyping and late-bound overloading
• Efficient execution in an automated reasoning environment
• scientific article; zbMATH DE number 3936465 (Why is no real title available?)
• Principles of programming with complex objects and collection types
• Semantic subtyping with an SMT solver
• Semantic subtyping, dealing set-theoretically with function, union, intersection, and negation types
• Simplify: a theorem prover for program checking
• Symbolic execution and program testing
• Termination of nested and mutually recursive algorithms
• Translating higher-order clauses to first-order clauses

Cited in

(6)

• Syntax-guided rewrite rule enumeration for SMT solvers
• Backward type inference for XML queries
• Information flow analysis for valued-indexed data security compartments
• Nested refinements: a logic for duck typing
• Semantic subtyping with an SMT solver
• Automata, Languages and Programming

Describes a project that uses

Uses Software

• SMT-LIB
• Eiffel

This page was built for publication: Semantic subtyping with an SMT solver

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