Elven
Contractor: FCT
Begin: 07/2016 - End: 07/2019
Partners: 2 partners
Project Contact: Mário Florido
Keywords: Type Systems and Program Verification
We approach data quality in the web as a verification problem. First, we address the richness and rapid evolution of web frameworks by defining a core language in which to compile different target data representation and processing languages, and which will be well suited for program verification. We shall start with the foundation of several reasoning tools: higher order logic. Then, we will take advantage of state-of-the-art theorem provers, declarative programming languages, and declarative database languages. The novelty of our approach is the use of higher-order logic as a common intermediate language suitable both for Web programming and to its formal verification and the verification of this core language combining the different complementary approaches of type-based verification mechanisms and more traditional verification techniques.
Information not available