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