Extracting Purely Functional Contents from Logical Inductive Types

DOI10.1007/978-3-540-74591-4_7zbMath1144.68354OpenAlexW1534887562MaRDI QIDQ3523167

Catherine Dubois, Jean-Frédéric Étienne, David Delahaye

Publication date: 2 September 2008

Published in: Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/978-3-540-74591-4_7

Mathematics Subject Classification ID

Related Items (3)

Turning Inductive into Equational Specifications ⋮ Mechanized semantics for the clight subset of the C language ⋮ A list-machine benchmark for mechanized metatheory

Uses Software

• Coq

This page was built for publication: Extracting Purely Functional Contents from Logical Inductive Types