A Formal Translation From an Imperative Language With Array to a Declarative Language

The main issue of this paper is to study the problem of formal translation of programs from an imperative language to a declarative one. To that end, we define a simple imperative language, denoted by L"1, that supports the basic types of statements ...

Model-based software engineering gains further attention these days. To better support it, the use of constraint languages is important in order to bridge expressiveness gaps and eliminate ambiguity. Nevertheless, the use of model-based constraint ...

We present a declarative language inspired by the pseudo-natural language previously used in Matita for the explanation of proof terms. We show how to compile the language to proof terms and how to automatically generate declarative scripts from proof ...