An programming language theory

Programming language theory

Programming language theory is a branch of computer science that deals with the design, implementation, analysis, characterization, and classification of programming languages and their individual features. It falls within the discipline of computer science, both depending on and affecting...

, the algebraic semantics of a programming language

Programming language

A programming language is an artificial language designed to communicate instructions to a machine, particularly a computer. Programming languages can be used to create programs that control the behavior of a machine and/or to express algorithms precisely....

 is a form of axiomatic semantics

Axiomatic semantics

Axiomatic semantics is an approach based on mathematical logic to proving the correctness of computer programs. It is closely related to Hoare logic....

 based on algebra

Algebra

Algebra is the branch of mathematics concerning the study of the rules of operations and relations, and the constructions and concepts arising from them, including terms, polynomials, equations and algebraic structures...

ic laws for describing and reasoning about program semantics in a formal

Formal methods

In computer science and software engineering, formal methods are a particular kind of mathematically-based techniques for the specification, development and verification of software and hardware systems...

 manner.

In mathematical logic

Mathematical logic

Mathematical logic is a subfield of mathematics with close connections to foundations of mathematics, theoretical computer science and philosophical logic. The field includes both the mathematical study of logic and the applications of formal logic to other areas of mathematics...

, algebraic semantics is a formal semantics based on algebras studied as part of algebraic logic

Algebraic logic

In mathematical logic, algebraic logic is the study of logic presented in an algebraic style.What is now usually called classical algebraic logic focuses on the identification and algebraic description of models appropriate for the study of various logics and connected problems...

. For example, the modal logic

Modal logic

Modal logic is a type of formal logic that extends classical propositional and predicate logic to include operators expressing modality. Modals — words that express modalities — qualify a statement. For example, the statement "John is happy" might be qualified by saying that John is...

 S4 is characterized by the class of topological boolean algebras

Interior algebra

In abstract algebra, an interior algebra is a certain type of algebraic structure that encodes the idea of the topological interior of a set. Interior algebras are to topology and the modal logic S4 what Boolean algebras are to set theory and ordinary propositional logic...

—that is, boolean algebras with an interior operator. Other modal logics are characterized by various other algebras with operators. The class of boolean algebras characterizes classical propositional logic, and the class of Heyting algebra

Heyting algebra

In mathematics, a Heyting algebra, named after Arend Heyting, is a bounded lattice equipped with a binary operation a→b of implication such that ∧a ≤ b, and moreover a→b is the greatest such in the sense that if c∧a ≤ b then c ≤ a→b...

s propositional intuitionistic logic

Intuitionistic logic

Intuitionistic logic, or constructive logic, is a symbolic logic system differing from classical logic in its definition of the meaning of a statement being true. In classical logic, all well-formed statements are assumed to be either true or false, even if we do not have a proof of either...

.

See also

• OBJ (programming language)
• Semantics of programming languages
  • Axiomatic semantics
    Axiomatic semantics
    Axiomatic semantics is an approach based on mathematical logic to proving the correctness of computer programs. It is closely related to Hoare logic....
    
    
  • Operational semantics
    Operational semantics
    In computer science, operational semantics is a way to give meaning to computer programs in a mathematically rigorous way. Operational semantics are classified into two categories: structural operational semantics formally describe how the individual steps of a computation take place in a...
    
    
  • Denotational semantics
    Denotational semantics
    In computer science, denotational semantics is an approach to formalizing the meanings of programming languages by constructing mathematical objects which describe the meanings of expressions from the languages...
    
    

Further reading

(2nd published by ASL

Association for Symbolic Logic

The Association for Symbolic Logic is an international organization of specialists in mathematical logic and philosophical logic—the largest such organization in the world. The ASL was founded in 1936, a crucial year in the development of modern logic, and its first president was Alonzo Church...

 in 2009) open access at Project Euclid Good introduction for readers with prior exposure to non-classical logic

Non-classical logic

Non-classical logics is the name given to formal systems which differ in a significant way from standard logical systems such as propositional and predicate logic. There are several ways in which this is done, including by way of extensions, deviations, and variations...

s but without much background in order theory

Order theory

Order theory is a branch of mathematics which investigates our intuitive notion of order using binary relations. It provides a formal framework for describing statements such as "this is less than that" or "this precedes that". This article introduces the field and gives some basic definitions...

 and/or universal algebra

Universal algebra

Universal algebra is the field of mathematics that studies algebraic structures themselves, not examples of algebraic structures....

; the book covers these prerequisites at length. The book however has been criticized for poor and sometimes incorrect presentation of AAL results. http://www.jstor.org/stable/3094793