Inductive types in constructive languages

Peter Johan de Bruin

Inductive types in constructive languages

Peter Johan de Bruin

Research output: Thesis › Thesis fully internal (DIV)

4128 Downloads (Pure)

Abstract

This dissertation deals with constructive languages: languages for the formal expression of mathematical constructions. The concept of construction does not only encompass computations, as expressed in programming languages,but also propositions and proofs, as expressed in a mathematical logic, and in particular the construction of structured mathematical objects like sequences and trees. Types may be conceived of as classes of such objects, and inductive types are types whose objects are generated by production rules ... Zie: Summary

Original language	English
Qualification	Doctor of Philosophy
Supervisors/Advisors	Renardel de Lavalette, Gerard, Supervisor
Publisher	s.n.
Publication status	Published - 1995

Keywords

Proefschriften (vorm)
Formele talen

Access to Document

titlecon.pdfFinal publisher's version, 164 KB
c1.pdfFinal publisher's version, 235 KB
c2.pdfFinal publisher's version, 316 KB
c3.pdfFinal publisher's version, 229 KB
c4.pdfFinal publisher's version, 269 KB
c5.pdfFinal publisher's version, 229 KB
c6.pdfFinal publisher's version, 237 KB
c7.pdfFinal publisher's version, 215 KB
c8.pdfFinal publisher's version, 203 KB
c9.pdfFinal publisher's version, 227 KB
c10.pdfFinal publisher's version, 204 KB
c11.pdfFinal publisher's version, 191 KB
appendic.pdfFinal publisher's version, 719 KB
appendix.pdfFinal publisher's version, 415 KB
bibliography.pdfFinal publisher's version, 150 KB
index.pdfFinal publisher's version, 202 KB
referenc.pdfFinal publisher's version, 144 KB
samenvat.pdfFinal publisher's version, 98.5 KB
stelling.pdfFinal publisher's version, 193 KB
summary.pdfFinal publisher's version, 82.7 KB
thesis.pdfFinal publisher's version, 1.43 MB

Handle.net

Persistent link

Cite this

@phdthesis{87db58af1fd64030a86298b5651d6be8,

title = "Inductive types in constructive languages",

abstract = "This dissertation deals with constructive languages: languages for the formal expression of mathematical constructions. The concept of construction does not only encompass computations, as expressed in programming languages,but also propositions and proofs, as expressed in a mathematical logic, and in particular the construction of structured mathematical objects like sequences and trees. Types may be conceived of as classes of such objects, and inductive types are types whose objects are generated by production rules ... Zie: Summary",

keywords = "Proefschriften (vorm), Formele talen",

author = "Bruin, \{Peter Johan de\}",

note = "date\_submitted:1996 Rights: University of Groningen",

year = "1995",

language = "English",

publisher = "s.n.",

}

TY - BOOK

T1 - Inductive types in constructive languages

AU - Bruin, Peter Johan de

N1 - date_submitted:1996 Rights: University of Groningen

PY - 1995

Y1 - 1995

N2 - This dissertation deals with constructive languages: languages for the formal expression of mathematical constructions. The concept of construction does not only encompass computations, as expressed in programming languages,but also propositions and proofs, as expressed in a mathematical logic, and in particular the construction of structured mathematical objects like sequences and trees. Types may be conceived of as classes of such objects, and inductive types are types whose objects are generated by production rules ... Zie: Summary

AB - This dissertation deals with constructive languages: languages for the formal expression of mathematical constructions. The concept of construction does not only encompass computations, as expressed in programming languages,but also propositions and proofs, as expressed in a mathematical logic, and in particular the construction of structured mathematical objects like sequences and trees. Types may be conceived of as classes of such objects, and inductive types are types whose objects are generated by production rules ... Zie: Summary

KW - Proefschriften (vorm)

KW - Formele talen

M3 - Thesis fully internal (DIV)

PB - s.n.

ER -

Inductive types in constructive languages

Abstract

Keywords

Access to Document

Handle.net

Fingerprint

Cite this