Type inference verified: Algorithm W in isabelle/HOL

Wolfgang Naraschewski; Tobias Nipkow

doi:10.1007/BFb0097799

Type inference verified: Algorithm W in isabelle/HOL

Wolfgang Naraschewski, Tobias Nipkow

Informatics 7 - Chair of Theoretical Computer Science

Technical University of Munich

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

1 Scopus citations

Original language	English
Title of host publication	Types for Proofs and Programs - International Workshop TYPES 1996, Selected Papers
Editors	Christine Paulin-Mohring, Eduardo Gimenez
Publisher	Springer Verlag
Pages	317-332
Number of pages	16
ISBN (Print)	3540651373, 9783540651376
DOIs	https://doi.org/10.1007/BFb0097799
State	Published - 1998
Event	1st International Workshop on Types for Proofs and Programs, TYPES 1996 - Aussois, France Duration: 15 Dec 1996 → 19 Dec 1996

Publication series

Name	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume	1512
ISSN (Print)	0302-9743
ISSN (Electronic)	1611-3349

Conference

Conference	1st International Workshop on Types for Proofs and Programs, TYPES 1996
Country/Territory	France
City	Aussois
Period	15/12/96 → 19/12/96

Access to Document

10.1007/BFb0097799

Cite this

Naraschewski, W., & Nipkow, T. (1998). Type inference verified: Algorithm W in isabelle/HOL. In C. Paulin-Mohring, & E. Gimenez (Eds.), Types for Proofs and Programs - International Workshop TYPES 1996, Selected Papers (pp. 317-332). (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1512). Springer Verlag. https://doi.org/10.1007/BFb0097799

Naraschewski, Wolfgang ; Nipkow, Tobias. / Type inference verified : Algorithm W in isabelle/HOL. Types for Proofs and Programs - International Workshop TYPES 1996, Selected Papers. editor / Christine Paulin-Mohring ; Eduardo Gimenez. Springer Verlag, 1998. pp. 317-332 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)).

@inproceedings{1dc5794dcb8a4a6dad455df0888ffc2f,

title = "Type inference verified: Algorithm W in isabelle/HOL",

author = "Wolfgang Naraschewski and Tobias Nipkow",

year = "1998",

doi = "10.1007/BFb0097799",

language = "English",

isbn = "3540651373",

series = "Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)",

publisher = "Springer Verlag",

pages = "317--332",

editor = "Christine Paulin-Mohring and Eduardo Gimenez",

booktitle = "Types for Proofs and Programs - International Workshop TYPES 1996, Selected Papers",

note = "1st International Workshop on Types for Proofs and Programs, TYPES 1996 ; Conference date: 15-12-1996 Through 19-12-1996",

}

Naraschewski, W & Nipkow, T 1998, Type inference verified: Algorithm W in isabelle/HOL. in C Paulin-Mohring & E Gimenez (eds), Types for Proofs and Programs - International Workshop TYPES 1996, Selected Papers. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), vol. 1512, Springer Verlag, pp. 317-332, 1st International Workshop on Types for Proofs and Programs, TYPES 1996, Aussois, France, 15/12/96. https://doi.org/10.1007/BFb0097799

Type inference verified: Algorithm W in isabelle/HOL. / Naraschewski, Wolfgang; Nipkow, Tobias.
Types for Proofs and Programs - International Workshop TYPES 1996, Selected Papers. ed. / Christine Paulin-Mohring; Eduardo Gimenez. Springer Verlag, 1998. p. 317-332 (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics); Vol. 1512).

Research output: Chapter in Book/Report/Conference proceeding › Conference contribution › peer-review

TY - GEN

T1 - Type inference verified

T2 - 1st International Workshop on Types for Proofs and Programs, TYPES 1996

AU - Naraschewski, Wolfgang

AU - Nipkow, Tobias

PY - 1998

Y1 - 1998

UR - http://www.scopus.com/inward/record.url?scp=84958987538&partnerID=8YFLogxK

U2 - 10.1007/BFb0097799

DO - 10.1007/BFb0097799

M3 - Conference contribution

AN - SCOPUS:84958987538

SN - 3540651373

SN - 9783540651376

T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)

SP - 317

EP - 332

BT - Types for Proofs and Programs - International Workshop TYPES 1996, Selected Papers

A2 - Paulin-Mohring, Christine

A2 - Gimenez, Eduardo

PB - Springer Verlag

Y2 - 15 December 1996 through 19 December 1996

ER -

Naraschewski W, Nipkow T. Type inference verified: Algorithm W in isabelle/HOL. In Paulin-Mohring C, Gimenez E, editors, Types for Proofs and Programs - International Workshop TYPES 1996, Selected Papers. Springer Verlag. 1998. p. 317-332. (Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)). doi: 10.1007/BFb0097799

Type inference verified: Algorithm W in isabelle/HOL

Publication series

Conference

Access to Document

Other files and links

Cite this