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

Institut für Softwaretechnik und Programmiersprachen

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.

Originalsprache	Englisch
Titel	IFL 2007: Implementation and Application of Functional Languages
Seitenumfang	20
Band	5083 LNCS
Herausgeber (Verlag)	Springer Verlag
Erscheinungsdatum	24.09.2008
Seiten	254-273
ISBN (Print)	978-3-540-85372-5
ISBN (elektronisch)	978-3-540-85373-2
DOIs	https://doi.org/10.1007/978-3-540-85373-2_15
Publikationsstatus	Veröffentlicht - 24.09.2008
Veranstaltung	19th International Symposium on Implementation and Application of Functional Languages - Freiburg, Deutschland Dauer: 21.09.1007 → 23.09.1007 Konferenznummer: 73632

UN SDGs

Dieser Output leistet einen Beitrag zu folgendem(n) Ziel(en) für nachhaltige Entwicklung

Zugriff auf Dokument

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

Andere Dateien und Links

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

Zitieren

@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. Bd. 5083 LNCS, Lecture Notes in Computer Science , Bd. 5083 LNCS, Springer Verlag, S. 254-273, 19th International Symposium on Implementation and Application of Functional Languages , Freiburg, Baden-Württemberg, Deutschland, 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. Band 5083 LNCS Springer Verlag, 2008. S. 254-273 (Lecture Notes in Computer Science ; Band 5083 LNCS).

Publikation: Kapitel in Büchern/Berichten/Konferenzbänden › Konferenzbeitrag › Begutachtung

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

Zugriff auf Dokument

Andere Dateien und Links

Fingerprint

Zitieren