Encoding natural semantics in Coq

DOI10.1007/3-540-60043-4_56zbMath1496.68119OpenAlexW1596425290MaRDI QIDQ5096388

Delphine Terrasse

Publication date: 16 August 2022

Published in: Algebraic Methodology and Software Technology (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-60043-4_56

Mathematics Subject Classification ID

Logic in computer science (03B70) Semantics in the theory of computing (68Q55) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Formalization of mathematics in connection with theorem provers (68V20)

Related Items

Executable structural operational semantics in Maude

Cites Work

• Theo: An interactive proof development system
• A framework for defining logics
• Type inference with simple subtypes
• A formulation of the simple theory of types
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item