Modules over relative monads for syntax and semantics
- Submitting institution
-
The University of Birmingham
- Unit of assessment
- 11 - Computer Science and Informatics
- Output identifier
- 48271282
- Type
- D - Journal article
- DOI
-
10.1017/S0960129514000103
- Title of journal
- Mathematical Structures in Computer Science
- Article number
- -
- First page
- 3
- Volume
- 26
- Issue
- 1
- ISSN
- 0960-1295
- Open access status
- Out of scope for open access requirements
- Month of publication
- December
- Year of publication
- 2014
- URL
-
-
- Supplementary information
-
-
- Request cross-referral to
- -
- Output has been delayed by COVID-19
- No
- COVID-19 affected output statement
- -
- Forensic science
- No
- Criminology
- No
- Interdisciplinary
- No
- Number of additional authors
-
0
- Research group(s)
-
-
- Citation count
- 1
- Proposed double-weighted
- No
- Reserve for an output with double weighting
- No
- Additional information
- Plotkin founded "Structural Operational Semantics (SOS)" to develop tools for reasoning about the computational behaviour of programming languages. His theory cannot handle languages with variable binding such as lambda calculus, ML, or Haskell. This paper overcomes this limitation by encompassing variable binding. It has been expanded to a fully-fledged SOS (“Reduction Monads and Their Signatures”, POPL 2020).
Secondly, the novel notion of "relative module" introduced here was employed by Fields Medalist Voevodsky in his theory of type theories (e.g., "C-system of a module over a Jf-relative monad"). The results are verified in the computer proof assistant Coq.
- Author contribution statement
- -
- Non-English
- No
- English abstract
- -