Derivation and inference of higher-order strictness types

Sjaak Smetsers*, Marko van Eekelen

*Corresponding author for this work

Research output: Contribution to journalArticleAcademicpeer-review

Abstract

We extend an existing first-order typing system for strictness analysis to the fully higher-order case, covering both the derivation system and the inference algorithm. The resulting strictness typing system has expressive capabilities far beyond that of traditional strictness analysis systems. This extension is developed with the explicit aim of formally proving soundness of higher-order strictness typing with respect to a natural operational semantics. A key aspect of our approach is the introduction of a proof assistant at an early stage, namely during development of the proof. As such, the theorem prover aids the design of the language theoretic concepts. The new results in combination with their formal proof can be seen as a case study towards the achievement of the long term PoplMark Challenge. The proof framework developed for this case study can furthermore be used in other typing system case studies. (C) 2015 Elsevier Ltd. All rights reserved.

Original languageEnglish
Pages (from-to)166-180
Number of pages15
JournalComputer Languages Systems & Structures
Volume44
DOIs
Publication statusPublished - Dec 2015

Keywords

  • Strictness analysis
  • Lambda calculus
  • Typing
  • Operational semantics
  • Automated theorem proving

Cite this

@article{0beab3f249fe4485b55a0a472c398b3e,
title = "Derivation and inference of higher-order strictness types",
abstract = "We extend an existing first-order typing system for strictness analysis to the fully higher-order case, covering both the derivation system and the inference algorithm. The resulting strictness typing system has expressive capabilities far beyond that of traditional strictness analysis systems. This extension is developed with the explicit aim of formally proving soundness of higher-order strictness typing with respect to a natural operational semantics. A key aspect of our approach is the introduction of a proof assistant at an early stage, namely during development of the proof. As such, the theorem prover aids the design of the language theoretic concepts. The new results in combination with their formal proof can be seen as a case study towards the achievement of the long term PoplMark Challenge. The proof framework developed for this case study can furthermore be used in other typing system case studies. (C) 2015 Elsevier Ltd. All rights reserved.",
keywords = "Strictness analysis, Lambda calculus, Typing, Operational semantics, Automated theorem proving",
author = "Sjaak Smetsers and {van Eekelen}, Marko",
year = "2015",
month = "12",
doi = "10.1016/j.cl.2015.07.004",
language = "English",
volume = "44",
pages = "166--180",
journal = "Computer Languages Systems & Structures",
issn = "1477-8424",
publisher = "PERGAMON-ELSEVIER SCIENCE LTD",

}

Derivation and inference of higher-order strictness types. / Smetsers, Sjaak; van Eekelen, Marko.

In: Computer Languages Systems & Structures, Vol. 44, 12.2015, p. 166-180.

Research output: Contribution to journalArticleAcademicpeer-review

TY - JOUR

T1 - Derivation and inference of higher-order strictness types

AU - Smetsers, Sjaak

AU - van Eekelen, Marko

PY - 2015/12

Y1 - 2015/12

N2 - We extend an existing first-order typing system for strictness analysis to the fully higher-order case, covering both the derivation system and the inference algorithm. The resulting strictness typing system has expressive capabilities far beyond that of traditional strictness analysis systems. This extension is developed with the explicit aim of formally proving soundness of higher-order strictness typing with respect to a natural operational semantics. A key aspect of our approach is the introduction of a proof assistant at an early stage, namely during development of the proof. As such, the theorem prover aids the design of the language theoretic concepts. The new results in combination with their formal proof can be seen as a case study towards the achievement of the long term PoplMark Challenge. The proof framework developed for this case study can furthermore be used in other typing system case studies. (C) 2015 Elsevier Ltd. All rights reserved.

AB - We extend an existing first-order typing system for strictness analysis to the fully higher-order case, covering both the derivation system and the inference algorithm. The resulting strictness typing system has expressive capabilities far beyond that of traditional strictness analysis systems. This extension is developed with the explicit aim of formally proving soundness of higher-order strictness typing with respect to a natural operational semantics. A key aspect of our approach is the introduction of a proof assistant at an early stage, namely during development of the proof. As such, the theorem prover aids the design of the language theoretic concepts. The new results in combination with their formal proof can be seen as a case study towards the achievement of the long term PoplMark Challenge. The proof framework developed for this case study can furthermore be used in other typing system case studies. (C) 2015 Elsevier Ltd. All rights reserved.

KW - Strictness analysis

KW - Lambda calculus

KW - Typing

KW - Operational semantics

KW - Automated theorem proving

U2 - 10.1016/j.cl.2015.07.004

DO - 10.1016/j.cl.2015.07.004

M3 - Article

VL - 44

SP - 166

EP - 180

JO - Computer Languages Systems & Structures

JF - Computer Languages Systems & Structures

SN - 1477-8424

ER -