School of Computing

The Sigma-Semantics: A Comprehensive Semantics for Functional Programs

Olaf Chitil

Fundamenta Informaticae, 31:182-196, 1997.

Abstract

A comprehensive semantics for functional programs is presented, which generalizes the well-known call-by-value and call-by-name semantics. By permitting a separate choice between call-by value and call-by-name for every argument position of every function and parameterizing the semantics by this choice we abstract from the parameter-passing mechanism. Thus common and distinguishing features of all instances of the sigma-semantics, especially call-by-value and call-by-name semantics, are highlighted. Furthermore, a property can be validated for all instances of the sigma-semantics by a single proof. This is employed for proving the equivalence of the given denotational (fixed-point based) and two operational (reduction based) definitions of the sigma-semantics. We present and apply means for very simple proofs of equivalence with the denotational sigma-semantics for a large class of reduction-based sigma-semantics. Our basis are simple first-order constructor-based functional programs with patterns.

Download publication 419 kbytes (PDF)

Bibtex Record

@article{1907,
author = {Olaf Chitil},
title = {{The Sigma-Semantics: A Comprehensive Semantics for Functional Programs}},
month = {unknown},
year = {1997},
pages = {182-196},
keywords = {determinacy analysis, Craig interpolants},
note = {},
doi = {},
url = {http://www.cs.kent.ac.uk/pubs/1997/1907},
    publication_type = {article},
    submission_id = {22114_1083674637},
    other_year = {1997},
    journal = {Fundamenta Informaticae},
    volume = {31},
    publisher = {IOS Press},
}

School of Computing, University of Kent, Canterbury, Kent, CT2 7NF

Enquiries: +44 (0)1227 824180 or contact us.

Last Updated: 21/03/2014