A list-machine benchmark for mechanized metatheory

DOI10.1007/s10817-011-9226-1zbMath1260.68362OpenAlexW2088975898MaRDI QIDQ1945921

Xavier Leroy, Robert Dockins, Andrew W. Appel

Publication date: 17 April 2013

Published in: Journal of Automated Reasoning (Search for Journal in Brave)

Full work available at URL: https://hal.inria.fr/hal-00674176

zbMATH Keywords

theorem provingproof assistantsprogram proofcompiler verificationmetatheory\texttt{Coq}\texttt{Twelf}typed machine language

Mathematics Subject Classification ID

Theory of programming languages (68N15) Theory of compilers and interpreters (68N20)

Related Items (3)

Fair enumeration combinators ⋮ Multimodal Separation Logic for Reasoning About Operational Semantics ⋮ A formalization of multi-tape Turing machines

Uses Software

• Coq
• Twelf
• PoplMark
• TALx86

Cites Work

• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Coinductive big-step operational semantics
• A syntactic approach to type soundness
• A very modal model of a modern, major, general type system
• Extracting Purely Functional Contents from Logical Inductive Types
• Stack-based typed assembly language
• Theorem Proving in Higher Order Logics

This page was built for publication: A list-machine benchmark for mechanized metatheory