A Short Isabelle/HOL Tutorial for the Functional Programmer

Thomas Genet 1
1 CELTIQUE - Software certification with semantic analysis
Inria Rennes – Bretagne Atlantique , IRISA-D4 - LANGAGE ET GÉNIE LOGICIEL
Abstract : The objective of this (very) short tutorial is to help any functional programmer to quickly put its hand on Isabelle/HOL and catch a glimpse of its power. Then, if you want some more, you should refer to the extensive Isabelle/HOL tutorial and documentation available in the tool.
Complete list of metadatas

https://hal.inria.fr/hal-01208577
Contributor : Thomas Genet <>
Submitted on : Tuesday, August 28, 2018 - 2:30:28 PM
Last modification on : Friday, September 13, 2019 - 9:48:42 AM
Long-term archiving on : Thursday, November 29, 2018 - 4:59:05 PM

File

main.pdf
Files produced by the author(s)

Identifiers

  • HAL Id : hal-01208577, version 6

Citation

Thomas Genet. A Short Isabelle/HOL Tutorial for the Functional Programmer. [Research Report] IRISA. 2017, pp.1-5. ⟨hal-01208577v6⟩

Share

Metrics

Record views

492

Files downloads

187