enter search term and/or author name
The intuitionism behind Statecharts steps
Gerald Lüttgen, Michael Mendler
The semantics of Statecharts macro steps, as introduced by Pnueli and Shalev , lacks compositionality. This article first analyzes the compositionality problem and traces it back to the invalidity of the Law of the Excluded Middle. It then...
Datalog LITE: a deductive query language with linear time model checking
Georg Gottlob, Erich Grädel, Helmut Veith
We present Datalog LITE, a new deductive query language with a linear-time model-checking algorithm, that is, linear time data complexity and program complexity. Datalog LITE is a variant of Datalog that uses stratified negation, restricted variable...
Reasoning with higher-order abstract syntax in a logical framework
Raymond C. McDowell, Dale A. Miller
Logical frameworks based on intuitionistic or linear logics with higher-type quantification have been successfully used to give high-level, modular, and formal specifications of many important judgments in the area of programming languages and...
Intuitionistic Light Affine Logic
Andrea Asperti, Luca Roversi
This article is a structured introduction to Intuitionistic Light Affine Logic (ILAL). ILAL has a polynomially costing normalization, and it is expressive enough to encode, and simulate, all PolyTime Turing machines. The bound on...