Operational Semantics
---------------------

<!--
SPDX-FileCopyrightText: Chris Pressey, the original author of this work, has dedicated it to the public domain.

SPDX-License-Identifier: CC0-1.0
-->

[(Up)](../../README.md#topics) | _Wikipedia: [Operational semantics](https://en.wikipedia.org/wiki/Operational_semantics)_ | _See also: [Formal Specification](../Formal%20Specification/README.md#formal-specification), [Programming Languages](../Programming%20Languages/README.md#programming-languages)_

- - - -

Works regarding the study of the semantics of systems given operationally, that is, given a set of permittable sequences of steps or (state transformations) of the system. The system in question is often the execution of a programming language.

### Web resources

[apfelmus - The Operational Monad Tutorial](https://apfelmus.nfshost.com/articles/operational-monad.html) ★


### Repositories

[thautwarm/Sequent.jl: formally and easily, describe the semantics.](https://github.com/thautwarm/Sequent.jl) ★★ [💭](commentary/cpressey.md#thautwarm-sequent-jl-formally-and-easily-describe-the-semantics)

_(in [Calculus of Constructions](../Calculus%20of%20Constructions/README.md#calculus-of-constructions))_ [wilbowma/cic-redex: A Redex model of CIC as specified in Chapter 4 of the Coq reference manual.](https://github.com/wilbowma/cic-redex) ★


### Papers

[An Introduction to Operational Semantics](https://www.cse.iitd.ac.in/~sak/courses/pl/opsem.pdf) ★★ [💭](commentary/cpressey.md#an-introduction-to-operational-semantics)

_(in [Theorem Proving](../Theorem%20Proving/README.md#theorem-proving))_ Theorem proving support in programming language semantics (online @ [arxiv.org](https://arxiv.org/abs/0707.0926)) ★ [💭](commentary/cpressey.md#theorem-proving-support-in-programming-language-semantics)