HM(X) type inference is CLP(X) solving
From MaRDI portal
Publication:5451969
Recommendations
- scientific article; zbMATH DE number 1089242
- Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L
- scientific article; zbMATH DE number 1301739
- Solving Horn clauses on inductive data types without induction
- Publication:4944893
- Type Inference by Coinductive Logic Programming
- An extension of HM(X) with bounded existential and universal data-types
- Weak completeness of type assignment in -calculus models: A generalization of Hindley's result
- scientific article; zbMATH DE number 2085172
- Solving Horn Clauses on Inductive Data Types Without Induction – ERRATUM
Cites work
- scientific article; zbMATH DE number 1952947 (Why is no real title available?)
- A Machine-Oriented Logic Based on the Resolution Principle
- A constraint-based region inference algorithm
- A framework for type inference with subtyping
- A polymorphic type system for Prolog
- A theory of type polymorphism in programming
- Concepts in Programming Languages
- Nominal unification
- The semantics of constraint logic programs1Note that reviewing of this paper was handled by the Editor-in-Chief.1
- Type inference with subtypes
Cited in
(8)- scientific article; zbMATH DE number 1420825 (Why is no real title available?)
- scientific article; zbMATH DE number 1692901 (Why is no real title available?)
- Proof-relevant Horn clauses for dependent type inference and term synthesis
- An extension of HM(X) with bounded existential and universal data-types
- Type inference using constraint handling rules
- Abstract compilation of object-oriented languages into coinductive CLP(X): can type inference meet verification?
- Type Processing by Constraint Reasoning
- Idealized coinductive type systems for imperative object-oriented programs
This page was built for publication: HM(X) type inference is CLP(X) solving
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5451969)
