From Contracts towards Dependent Types: Proofs by Partial Evaluation

Stephan Herhut; Sven Bodo Scholz; Robert Bernecky; Clemens Grelck; Kai Trojahner

doi:10.1007/978-3-540-85373-2_15

From Contracts towards Dependent Types: Proofs by Partial Evaluation

Stephan Herhut, Sven Bodo Scholz, Robert Bernecky, Clemens Grelck, Kai Trojahner

Institute of Software Engineering and Programming Languages

Abstract

The specification and resolution of non-trivial domain constraints has become a well-recognised measure for improving the stability of large software systems. In this paper we propose an approach based on partial evaluation which tries to prove such constraints statically as far as possible and inserts efficient dynamic checks otherwise.

Original language	English
Title of host publication	IFL 2007: Implementation and Application of Functional Languages
Number of pages	20
Volume	5083 LNCS
Publisher	Springer Verlag
Publication date	24.09.2008
Pages	254-273
ISBN (Print)	978-3-540-85372-5
ISBN (Electronic)	978-3-540-85373-2
DOIs	https://doi.org/10.1007/978-3-540-85373-2_15
Publication status	Published - 24.09.2008
Event	19th International Symposium on Implementation and Application of Functional Languages - Freiburg, Germany Duration: 21.09.1007 → 23.09.1007 Conference number: 73632

UN SDGs

This output contributes to the following UN Sustainable Development Goals (SDGs)

Access to Document

10.1007/978-3-540-85373-2_15

Cite this

@inproceedings{351fcf075eb04e2f91c19b577966f8b6,

title = "From Contracts towards Dependent Types: Proofs by Partial Evaluation",

abstract = "The specification and resolution of non-trivial domain constraints has become a well-recognised measure for improving the stability of large software systems. In this paper we propose an approach based on partial evaluation which tries to prove such constraints statically as far as possible and inserts efficient dynamic checks otherwise.",

author = "Stephan Herhut and Scholz, {Sven Bodo} and Robert Bernecky and Clemens Grelck and Kai Trojahner",

year = "2008",

month = sep,

day = "24",

doi = "10.1007/978-3-540-85373-2_15",

language = "English",

isbn = "978-3-540-85372-5",

volume = "5083 LNCS",

series = "Lecture Notes in Computer Science ",

publisher = "Springer Verlag",

pages = "254--273",

booktitle = "IFL 2007: Implementation and Application of Functional Languages",

note = "19th International Symposium on Implementation and Application of Functional Languages , IFL 2007 ; Conference date: 21-09-1007 Through 23-09-1007",

}

Herhut, S, Scholz, SB, Bernecky, R, Grelck, C & Trojahner, K 2008, From Contracts towards Dependent Types: Proofs by Partial Evaluation. in IFL 2007: Implementation and Application of Functional Languages. vol. 5083 LNCS, Lecture Notes in Computer Science , vol. 5083 LNCS, Springer Verlag, pp. 254-273, 19th International Symposium on Implementation and Application of Functional Languages , Freiburg, Baden-Württemberg, Germany, 21.09.07. https://doi.org/10.1007/978-3-540-85373-2_15

From Contracts towards Dependent Types: Proofs by Partial Evaluation. / Herhut, Stephan; Scholz, Sven Bodo; Bernecky, Robert et al.
IFL 2007: Implementation and Application of Functional Languages. Vol. 5083 LNCS Springer Verlag, 2008. p. 254-273 (Lecture Notes in Computer Science ; Vol. 5083 LNCS).

Research output: Chapters in Books/Reports/Conference Proceedings › Conference contribution › peer-review

TY - GEN

T1 - From Contracts towards Dependent Types: Proofs by Partial Evaluation

AU - Herhut, Stephan

AU - Scholz, Sven Bodo

AU - Bernecky, Robert

AU - Grelck, Clemens

AU - Trojahner, Kai

N1 - Conference code: 73632

PY - 2008/9/24

Y1 - 2008/9/24

N2 - The specification and resolution of non-trivial domain constraints has become a well-recognised measure for improving the stability of large software systems. In this paper we propose an approach based on partial evaluation which tries to prove such constraints statically as far as possible and inserts efficient dynamic checks otherwise.

AB - The specification and resolution of non-trivial domain constraints has become a well-recognised measure for improving the stability of large software systems. In this paper we propose an approach based on partial evaluation which tries to prove such constraints statically as far as possible and inserts efficient dynamic checks otherwise.

UR - https://www.scopus.com/record/display.uri?eid=2-s2.0-52049084849&origin=inward&txGid=8015c3a651608b85a30e66ee48a5977d

U2 - 10.1007/978-3-540-85373-2_15

DO - 10.1007/978-3-540-85373-2_15

M3 - Conference contribution

SN - 978-3-540-85372-5

VL - 5083 LNCS

T3 - Lecture Notes in Computer Science

SP - 254

EP - 273

BT - IFL 2007: Implementation and Application of Functional Languages

PB - Springer Verlag

T2 - 19th International Symposium on Implementation and Application of Functional Languages

Y2 - 21 September 1007 through 23 September 1007

ER -

From Contracts towards Dependent Types: Proofs by Partial Evaluation

Abstract

UN SDGs

Access to Document

Other files and links

Fingerprint

Cite this