Semantics (computer science)

In programming language theory, semantics is the rigorous mathematical study of the meaning of programming languages. Semantics assigns computational meaning to valid strings in a programming language syntax. It is closely related to, and often crosses over with, the semantics of mathematical proofs. Semantics describes the processes a computer follows when executing a program in that specific language. This can be shown by describing the relationship between the input and output of a program, or an explanation of how the program will be executed on a certain platform, hence creating a model of computation. In 1967, Robert W. Floyd publishes the paper Assigning meanings to programs; his chief aim is "a rigorous standard for proofs about computer programs, including proofs of correctness, equivalence, and termination". Floyd further writes: A semantic definition of a programming language, in our approach, is founded on a syntactic definition. It must specify which of the phrases in a syntactically correct program represent commands, and what conditions must be imposed on an interpretation in the neighborhood of each command. In 1969, Tony Hoare publishes a paper on Hoare logic seeded by Floyd's ideas, now sometimes collectively called axiomatic semantics. In the 1970s, the terms operational semantics and denotational semantics emerged. The field of formal semantics encompasses all of the following: The definition of semantic models The relations between different semantic models The relations between different approaches to meaning The relation between computation and the underlying mathematical structures from fields such as logic, set theory, model theory, , etc. It has close links with other areas of computer science such as programming language design, type theory, compilers and interpreters, program verification and model checking. There are many approaches to formal semantics; these belong to three major classes: Denotational semantics, whereby each phrase in the language is interpreted as a denotation, i.e.

About this result

This page is automatically generated and may contain information that is not correct, complete, up-to-date, or relevant to your search query. The same applies to every other page on this website. Please make sure to verify the information with EPFL's official sources.

Related concepts (57)

Related courses (7)

Related lectures (56)

CS-452: Foundations of software

The course introduces the foundations on which programs and programming languages are built. It introduces syntax, types and semantics as building blocks that together define the properties of a progr

CS-550: Formal verification

We introduce formal verification as an approach for developing highly reliable systems. Formal verification finds proofs that computer systems work under all relevant scenarios. We will learn how to u

CS-320: Computer language processing

We teach the fundamental aspects of analyzing and interpreting computer languages, including the techniques to build compilers. You will build a working compiler from an elegant functional language in

Low-level programming language

A low-level programming language is a programming language that provides little or no abstraction from a computer's instruction set architecture—commands or functions in the language map that are structurally similar to processor's instructions. Generally, this refers to either machine code or assembly language. Because of the low (hence the word) abstraction between the language and machine language, low-level languages are sometimes described as being "close to the hardware".

Operational semantics

Operational semantics is a category of formal programming language semantics in which certain desired properties of a program, such as correctness, safety or security, are verified by constructing proofs from logical statements about its execution and procedures, rather than by attaching mathematical meanings to its terms (denotational semantics).

Object-oriented programming

Object-Oriented Programming (OOP) is a programming paradigm based on the concept of "objects", which can contain data and code. The data is in the form of fields (often known as attributes or properties), and the code is in the form of procedures (often known as methods). A common feature of objects is that procedures (or methods) are attached to them and can access and modify the object's data fields. In this brand of OOP, there is usually a special name such as or used to refer to the current object.

Covers Amyli, a tiny functional language, type rules, and soundness.

Explores music semantics, discussing inferences triggered by different musical elements and proposing a framework for understanding music's meaning.

Explores Church numerals, Booleans, pairs, recursion, and behavioral equivalence in Lambda Calculus.