Applied Lambda calculus. Using a type theory based proof assistant

dc.contributor.author	Pretorius, L
dc.date.accessioned	2018-06-06T13:50:09Z
dc.date.available	2018-06-06T13:50:09Z
dc.date.issued	1998
dc.identifier.citation	Pretorius L (1998) Applied Lambda calculus. Using a type theory based proof assistant. South African Computer Journal, Number 21, 1998	en
dc.identifier.issn	2313-7835
dc.identifier.uri	http://hdl.handle.net/10500/24286
dc.description.abstract	We introduce a number of typed lambda calculi, show how type theory may be used as basis for a proof assistant, and illustrate this with the Coq proof assistant.	en
dc.language.iso	en	en
dc.publisher	South African Computer Society (SAICSIT)	en
dc.subject	Applied lambda calculus	en
dc.subject	Type theory	en
dc.subject	Proof assistants	en
dc.subject	Coq	en
dc.title	Applied Lambda calculus. Using a type theory based proof assistant	en
dc.type	Article	en