Documentation

The manual for the lastest release

The reference manual for the FoCaLiZe language and system:

• refman.ps, size 1MB, (in PS format).
• refman.pdf, size 652KB, (in PDF format).
• refman.dvi, size 476KB, (in DVI format).

Programming and Proving: Practice with FoCaLiZe

A course in FoCaLiZe given in May 2014 at Ecole des Jeunes Chercheurs en Programmation (EJCP, doctoral summer school) :

• Slides in PDF.
• Lecture notes in PDF.

Tutorial: Implementing Sets

A tutorial for the FoCaLiZe language and system:

• tutorial.ps, size , (in PS format).
• tutorial.pdf, size , (in PDF format).
• tutorial.dvi, size , (in DVI format).

Tutorial: Playing with Proofs (Updated -- still few words to add) on 2014-03-06)

A tutorial for the FoCaLiZe language especially dedicated to proofs writing (these online versions are more recent than those of the distribution):

• tuto_proofs.ps, size , (in PS format).
• tuto_proofs.pdf, size , (in PDF format).
• tuto_proofs.dvi, size , (in DVI format).

The manual pages for the FoCaLiZe commands

• The manual for the focalizec compiler (Unix man page).
• The manual for the focalizedep make dependencies compiler (Unix man page).

Older versions

The previous versions of FoCaLiZe documentation are still available in the oldies directory.