Semantic subtyping for declarative data scripting language by calling a prover
US8413119B2 · kind B2 · utility
Assignee
Inventors
Key dates
| Filing date | Oct 3, 2008 |
| Grant date | Apr 2, 2013 |
| Priority date | — |
| Expiry date | Jan 17, 2032 |
Classification
- Technology area (CPC G)Physics
- CPC primaryG06F8/437
- WIPO fieldComputer technology
- WIPO sectorElectrical engineering
Abstract
An efficient, logical and expressive type system supports the combination of refinement types and type membership expressions, as well as a top type that encompasses all valid values as members. Various embodiments verify the validity of subtyping relationships by translating to first-order logic, and invoking a general-purpose theorem prover with the first-order logic as input. In contrast to treating formulas as types, types are translated into formulas of standard first-order logic. Moreover, to represent data structures of the programming language as first-order logic, universal and existential quantifiers of first-order logic, and function symbols in terms, are exploited. Data intensive applications can be generated, verified, and deployed with greater speed and scale.
Source: USPTO / EPO open patent data. Objective bibliographic and citation counts.