Semantic subtyping with an SMT solver

DOI10.1017/S0956796812000032zbMath1248.68131OpenAlexW2106142143MaRDI QIDQ2913944

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

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)

Related Items (2)

Backward type inference for XML queries ⋮ Information Flow Analysis for Valued-Indexed Data Security Compartments

Uses Software

• Eiffel
• SMT-LIB

Cites Work

• Unnamed Item
• Principles of programming with complex objects and collection types
• A syntactic approach to type soundness
• Termination of nested and mutually recursive algorithms
• Dependent types with subtyping and late-bound overloading
• Translating higher-order clauses to first-order clauses
• Deciding validity in a spatial logic for trees
• Semantic subtyping
• Simplify: a theorem prover for program checking
• Symbolic execution and program testing
• Semantic subtyping with an SMT solver
• Efficient execution in an automated reasoning environment

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