Imperative Functional Programming with Isabelle/HOL.

Lukas Bulwahn Alexander Krauss Florian Haftmann Levent Erkök John Matthews

Published in: TPHOLs (2008)

Keyphrases

functional programming
theorem prover
natural deduction
inference rules
functional language
execution model
theorem proving
quantifier elimination
object oriented programming
programming language
sequent calculus
proof search
object oriented
first order logic
database systems
proof planning