Hybrid. A definitional two-level approach to reasoning with higher-order abstract syntax
From MaRDI portal
Publication:438569
DOI10.1007/s10817-010-9194-xzbMath1252.68252MaRDI QIDQ438569
Alberto Momigliano, Amy P. Felty
Publication date: 31 July 2012
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Full work available at URL: https://doi.org/10.1007/s10817-010-9194-x
induction; higher-order abstract syntax; Isabelle/HOL; interactive theorem proving; logical frameworks; Coq; variable binding
03B70: Logic in computer science
Uses Software