[TYPES/announce] CfP: Isabelle Tutorial at ITP in Nanjing

[Tobias Nipkow]

			   Call for Participation
		       -- Isabelle Tutorial at ITP --
			August 21-23, Nanjing, China
	
This intensive 3-day tutorial is aimed both at theorem proving novices and at
people already familiar with another proof assistant who want to learn about
Isabelle. The tutorial consists of a mixture of interactive lectures and
hands-on lab sessions where the participants solve theorem proving problems
with Isabelle. The following material is covered:

- A Functional Programming introduction to theorem proving:
   Data types, recursive functions and proof by induction
- Beyond equality: logic and set theory
- Isabelle's automatic proof toolbox
- Isar: a language for writing structured and readable proofs

The tutorial http://www.in.tum.de/~nipkow/isa-tut-itp15.html directly
precedes ITP 2015 http://www.inf.kcl.ac.uk/staff/urbanc/itp-2015/.
Registration is part of the ITP conference registration process.

-------------- next part --------------
A non-text attachment was scrubbed...
Name: smime.p7s
Type: application/pkcs7-signature
Size: 5112 bytes
Desc: S/MIME Cryptographic Signature
URL: <http://lists.seas.upenn.edu/pipermail/types-announce/attachments/20150713/f5dc9c46/attachment.p7s>