Browse DORAS
Browse Theses
Search
Latest Additions
Creative Commons License
Except where otherwise noted, content on this site is licensed for use under a:

Implementation of action semantics in coq

Ward, Sandra (1996) Implementation of action semantics in coq. Master of Science thesis, Dublin City University.

Full text available as:

[img]PDF - Requires a PDF viewer such as GSview, Xpdf or Adobe Acrobat Reader
2060Kb

Abstract

Formal Semantics is a topic of major importance in the study of programming language design. Action semantics is a recently developed framework for the specification of formal semantics which allows understandable, modular and reusable semantic descriptions of programming languages. Action laws are algebraic properties of primitive actions and action combinators which can be used to prove the existence of semantic equivalence between pairs of constructs, expressions etc. of programming language. This thesis endeavours to show how action semantics can be formalised computationally by reporting on the representation of the kernel of action notation in CAML. CAML is a functional language whose type systems allow the user to define his/her own data structures. It allows the definitions of functions manipulating these data structures with the security provided by strict type verification. The representation of the kernel in the specification language of the Coq development system is also outlined. The Coq system is an implementation of the Calculus of Inductive Constructions and provides goal-directed tactic-driven proof search. The proof engine of the Coq system is then used to prove various action laws.

Item Type:Thesis (Master of Science)
Date of Award:1996
Refereed:No
Supervisor(s):Power, James
Uncontrolled Keywords:Semantics; Syntax; Formal methods; Programming languages; Language design
Subjects:Computer Science > Software engineering
DCU Faculties and Centres:DCU Faculties and Schools > Faculty of Engineering and Computing > School of Computing
Use License:This item is licensed under a Creative Commons Attribution-NonCommercial-No Derivative Works 3.0 License. View License
ID Code:19464
Deposited On:03 Oct 2013 16:11 by Celine Campbell. Last Modified 03 Oct 2013 16:11

Download statistics

Archive Staff Only: edit this record