Operational Semantics of an Imperative Language in Definite Clauses

Research output: Chapter in Book/Report/Conference proceedingArticle in proceedingsResearchpeer-review

72 Downloads (Pure)


We present the “big-step” operational semantics of a small programming language NIL (Natural Imperative Language) in definite clauses, thus building on the fixpoint semantics of logic programs. NIL operates on a state which is just a sequence of counters. As basic statements NIL has incrementation, decrementation and test for null. NIL allows for sequential composition and non-deterministic choice of statements as well as mutually recursive definitions of procedures, which we find support our long-term aim of formalizing and reasoning about specific actions and planning tasks for rational agents. A novelty is the use of the de Bruijn notation instead of names. To our knowledge the operational semantics of an imperative language like NIL have not been given in definite clauses, although it is well-known that it is possible.
Original languageEnglish
Title of host publication2003 Joint Conference on Declarative Programming, AGP-2003, Reggio Calabria, Italy, September 3-5, 2003
EditorsFrancesco Buccafurri
Publication date2003
Publication statusPublished - 2003
Externally publishedYes
EventAPPIA-GULP-PRODE Joint Conference on Declarative Programming (AGP 3003) - Reggio Calabria, Italy
Duration: 3 Sept 20035 Sept 2003


ConferenceAPPIA-GULP-PRODE Joint Conference on Declarative Programming (AGP 3003)
CityReggio Calabria


Dive into the research topics of 'Operational Semantics of an Imperative Language in Definite Clauses'. Together they form a unique fingerprint.

Cite this