Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L
From MaRDI portal
Publication:1961917
DOI10.1023/A:1006277616879zbMath0943.68150MaRDI QIDQ1961917
Tobias Nipkow, Wolfgang Naraschewski
Publication date: 11 September 2000
Published in: Journal of Automated Reasoning (Search for Journal in Brave)
Functional programming and lambda calculus (68N18) Specification and verification (program logics, model checking, etc.) (68Q60)
Related Items (4)
Verified bytecode verification and type-certifying compilation ⋮ Code-carrying theories ⋮ A certified implementation of ML with structural polymorphism and recursive types ⋮ General Bindings and Alpha-Equivalence in Nominal Isabelle
Uses Software
This page was built for publication: Type inference verified: Algorithm \(\mathcal W\) in Isabelle/H0L
