Higher-Order Abstract Syntax in Isabelle/HOL

13 years 2 months ago

Download www.cs.utexas.edu

rder Abstract Syntax in Isabelle/HOL Douglas J. Howe Carleton University July 13, 2010 Douglas J. Howe (Carleton University) HOAS in Isabelle/HOL July 13, 2010 1 / 8

Douglas J. Howe

Real-time Traffic

ITP 2010 | Mathematics | Rder Abstract Syntax |

claim paper

» Verifying the CPS Transformation in IsabelleHOL

» Verifying CPS transformations in IsabelleHOL

» Formalizing a Framework for Dynamic Slicing of Program Dependence Graphs in IsabelleHOL

» Partial Recursive Functions in HigherOrder Logic

» Code Generation via HigherOrder Rewrite Systems

» HigherOrder Separation Logic in IsabelleHOLCF

» FreeStyle Theorem Proving

» Reasoning on an imperative objectbased calculus in Higher Order Abstract Syntax

Post Info
More Details (n/a)

Added	28 Jan 2011
Updated	28 Jan 2011
Type	Journal
Year	2010
Where	ITP
Authors	Douglas J. Howe

Comments (0)

Sciweavers

Higher-Order Abstract Syntax in Isabelle/HOL

ITP 2010 | Mathematics | Rder Abstract Syntax |

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers