Paper Info
Title
A higher-order logical framework for the algorithmic debugging and verification of declarative programs
Abstract
We propose a higher-order logical framework for declarative programming as an extension to the setting of the simply typed lambda calculus of a first-order rewriting logic, where programs are now presented by conditional pattern rewrite systems on lambda abstractions. We use this new logical framework to obtain a natural model-theoretic semantics from traditional theories in higher-order declarative (functional and logic) programming, and we provide a fixpoint semantics that matches the pattern model of a program as the least fixpoint of an operator defined over pattern algebras. We use this higher-order semantic framework as a basis for the verification of declarative programs and the development of efficient algorithmic debugging techniques. Our debugging approach proceeds by exploring an abridged computational tree built on a higher-order proof calculus with lambda abstractions that provides a purely declarative view of the computation, in order to detect a function rule that is incorrect in the intended model of the program's semantics. For verification purposes, our higher-order logical framework can be mapped into higher-order logic programming, and we can use this translation as a starting point to explore how to prove properties valid in the least pattern model of a program by means of different existing interactive proof assistants, as the Isabelle theorem prover.
Year
DOI
Venue
2009
10.1145/1599410.1599418
PPDP
Keywords
Field
DocType
higher-order declarative,lambda abstraction,higher-order proof calculus,higher-order semantic framework,higher-order logical framework,declarative program,higher-order logic programming,pattern model,algorithmic debugging,conditional pattern,declarative programming,typed lambda calculus,higher order,higher order logic,logical framework,theorem prover,lambda calculus,first order,rewriting logic
Lambda calculus,Programming language,Typed lambda calculus,Simply typed lambda calculus,Computer science,Proof calculus,Theoretical computer science,Logic programming,Declarative programming,Logical framework,Algorithmic program debugging
Conference
Citations 
PageRank 
References 
4
0.45
18
Authors
1
Name
Order
Citations
PageRank
Rafael del Vado V́ırseda19713.26