Programs, proofs and parametrized specifications

Iman Poernomo; John N Crossley; Martin Wirsing

doi:10.1007/3-540-45645-7_14

Programs, proofs and parametrized specifications

Iman Poernomo, John N Crossley, Martin Wirsing

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

Abstract

In a series of papers we have been using a modification of the ideas of Curry and Howard to obtain reliable programs from formal proofs. In this paper we extend our earlier work by presenting a new approach for constructing correct SML structures and SML functors from CASL structured and parametrized Specifications by extracting the SML programs from constructive proofs of the axioms of the specifications. We provide a novel formal calculus with rules corresponding to the construction and instantiation of parametrized Specifications and then a program extraction procedure which produces SML programs that meet their Specifications.

Original language	English
Title of host publication	Recent Trends in Algebraic Development Techniques
Subtitle of host publication	15th International Workshop, WADT 2001 Joint with the CoFI WG Meeting Genova, Italy, April 1-3, 2001 Selected Papers
Editors	Maura Cerioli, Gianna Reggio
Place of Publication	Berlin Germany
Publisher	Springer
Pages	280-304
Number of pages	25
ISBN (Print)	3540431594
DOIs	https://doi.org/10.1007/3-540-45645-7_14
Publication status	Published - 2001
Event	International Workshop on Algebraic Development Techniques 2001 - Genova, Italy Duration: 1 Apr 2001 → 3 Apr 2001 Conference number: 15th https://link.springer.com/book/10.1007/3-540-45645-7 (Proceedings)

Publication series

Name	Lecture Notes in Computer Science
Publisher	Springer
Volume	2267
ISSN (Print)	0302-9743

Conference

Conference	International Workshop on Algebraic Development Techniques 2001
Abbreviated title	WADT 2001
Country/Territory	Italy
City	Genova
Period	1/04/01 → 3/04/01
Internet address	https://link.springer.com/book/10.1007/3-540-45645-7 (Proceedings)

Access to Document

10.1007/3-540-45645-7_14

Cite this

Poernomo, I., Crossley, J. N., & Wirsing, M. (2001). Programs, proofs and parametrized specifications. In M. Cerioli, & G. Reggio (Eds.), Recent Trends in Algebraic Development Techniques: 15th International Workshop, WADT 2001 Joint with the CoFI WG Meeting Genova, Italy, April 1-3, 2001 Selected Papers (pp. 280-304). (Lecture Notes in Computer Science; Vol. 2267). Springer. https://doi.org/10.1007/3-540-45645-7_14

Poernomo, Iman ; Crossley, John N ; Wirsing, Martin. / Programs, proofs and parametrized specifications. Recent Trends in Algebraic Development Techniques: 15th International Workshop, WADT 2001 Joint with the CoFI WG Meeting Genova, Italy, April 1-3, 2001 Selected Papers. editor / Maura Cerioli ; Gianna Reggio. Berlin Germany : Springer, 2001. pp. 280-304 (Lecture Notes in Computer Science).

@inproceedings{e161b8c66e4b4dafb9ac8ef3ff7159ca,

title = "Programs, proofs and parametrized specifications",

abstract = "In a series of papers we have been using a modification of the ideas of Curry and Howard to obtain reliable programs from formal proofs. In this paper we extend our earlier work by presenting a new approach for constructing correct SML structures and SML functors from CASL structured and parametrized Specifications by extracting the SML programs from constructive proofs of the axioms of the specifications. We provide a novel formal calculus with rules corresponding to the construction and instantiation of parametrized Specifications and then a program extraction procedure which produces SML programs that meet their Specifications.",

author = "Iman Poernomo and Crossley, \{John N\} and Martin Wirsing",

year = "2001",

doi = "10.1007/3-540-45645-7\_14",

language = "English",

isbn = "3540431594",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "280--304",

editor = "Maura Cerioli and Gianna Reggio",

booktitle = "Recent Trends in Algebraic Development Techniques",

address = "Switzerland",

note = "International Workshop on Algebraic Development Techniques 2001, WADT 2001 ; Conference date: 01-04-2001 Through 03-04-2001",

url = "https://link.springer.com/book/10.1007/3-540-45645-7",

}

Poernomo, I, Crossley, JN & Wirsing, M 2001, Programs, proofs and parametrized specifications. in M Cerioli & G Reggio (eds), Recent Trends in Algebraic Development Techniques: 15th International Workshop, WADT 2001 Joint with the CoFI WG Meeting Genova, Italy, April 1-3, 2001 Selected Papers. Lecture Notes in Computer Science, vol. 2267, Springer, Berlin Germany, pp. 280-304, International Workshop on Algebraic Development Techniques 2001, Genova, Italy, 1/04/01. https://doi.org/10.1007/3-540-45645-7_14

Programs, proofs and parametrized specifications. / Poernomo, Iman; Crossley, John N; Wirsing, Martin.
Recent Trends in Algebraic Development Techniques: 15th International Workshop, WADT 2001 Joint with the CoFI WG Meeting Genova, Italy, April 1-3, 2001 Selected Papers. ed. / Maura Cerioli; Gianna Reggio. Berlin Germany: Springer, 2001. p. 280-304 (Lecture Notes in Computer Science; Vol. 2267).

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

TY - GEN

T1 - Programs, proofs and parametrized specifications

AU - Poernomo, Iman

AU - Crossley, John N

AU - Wirsing, Martin

N1 - Conference code: 15th

PY - 2001

Y1 - 2001

N2 - In a series of papers we have been using a modification of the ideas of Curry and Howard to obtain reliable programs from formal proofs. In this paper we extend our earlier work by presenting a new approach for constructing correct SML structures and SML functors from CASL structured and parametrized Specifications by extracting the SML programs from constructive proofs of the axioms of the specifications. We provide a novel formal calculus with rules corresponding to the construction and instantiation of parametrized Specifications and then a program extraction procedure which produces SML programs that meet their Specifications.

AB - In a series of papers we have been using a modification of the ideas of Curry and Howard to obtain reliable programs from formal proofs. In this paper we extend our earlier work by presenting a new approach for constructing correct SML structures and SML functors from CASL structured and parametrized Specifications by extracting the SML programs from constructive proofs of the axioms of the specifications. We provide a novel formal calculus with rules corresponding to the construction and instantiation of parametrized Specifications and then a program extraction procedure which produces SML programs that meet their Specifications.

U2 - 10.1007/3-540-45645-7_14

DO - 10.1007/3-540-45645-7_14

M3 - Conference Paper

SN - 3540431594

T3 - Lecture Notes in Computer Science

SP - 280

EP - 304

BT - Recent Trends in Algebraic Development Techniques

A2 - Cerioli, Maura

A2 - Reggio, Gianna

PB - Springer

CY - Berlin Germany

T2 - International Workshop on Algebraic Development Techniques 2001

Y2 - 1 April 2001 through 3 April 2001

ER -

Poernomo I, Crossley JN, Wirsing M. Programs, proofs and parametrized specifications. In Cerioli M, Reggio G, editors, Recent Trends in Algebraic Development Techniques: 15th International Workshop, WADT 2001 Joint with the CoFI WG Meeting Genova, Italy, April 1-3, 2001 Selected Papers. Berlin Germany: Springer. 2001. p. 280-304. (Lecture Notes in Computer Science). doi: 10.1007/3-540-45645-7_14