An embedding of Ruby in Isabelle

DOI10.1007/3-540-61511-3_80zbMath1412.68255OpenAlexW1540629521MaRDI QIDQ4647513

Ole Hjorth Rasmussen

Publication date: 15 January 2019

Published in: Automated Deduction — Cade-13 (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1007/3-540-61511-3_80

zbMATH Keywords

VLSI designconservative extensionZermelo-Fraenkel set theoryIsabelleparallel compositionRubygraphical interpretationtype rule

Mathematics Subject Classification ID

Axiomatics of classical set theory and its fragments (03E30)

Uses Software

• Isabelle
• ML
• Isabelle/ZF
• HOL

Cites Work

• Unnamed Item
• Unnamed Item
• A theory of type polymorphism in programming
• Set theory for verification. I: From foundations to functions
• Isabelle. A generic theorem prover
• A fixedpoint approach to implementing (Co)inductive definitions

This page was built for publication: An embedding of Ruby in Isabelle