### Skapa referens, olika format (klipp och klistra)

**Harvard**

Owens, S., Myreen, M., Kumar, R. och Tan, Y. (2016) *Functional big-step semantics*.

** BibTeX **

@conference{

Owens2016,

author={Owens, S. and Myreen, Magnus O. and Kumar, R. and Tan, Y.K.},

title={Functional big-step semantics},

booktitle={Lecture Notes in Computer Science; 25th European Symposium on Programming (ESOP)},

isbn={9783662494974},

pages={589-615},

abstract={When doing an interactive proof about a piece of software, it is important that the underlying programming language’s semantics does not make the proof unnecessarily difficult or unwieldy. Both smallstep and big-step semantics are commonly used, and the latter is typically given by an inductively defined relation. In this paper, we consider an alternative: using a recursive function akin to an interpreter for the language. The advantages include a better induction theorem, less duplication, accessibility to ordinary functional programmers, and the ease of doing symbolic simulation in proofs via rewriting. We believe that this style of semantics is well suited for compiler verification, including proofs of divergence preservation. We do not claim the invention of this style of semantics: our contribution here is to clarify its value, and to explain how it supports several language features that might appear to require a relational or small-step approach. We illustrate the technique on a simple imperative language with C-like for-loops and a break statement, and compare it to a variety of other approaches. We also provide ML and lambda-calculus based examples to illustrate its generality.},

year={2016},

}

** RefWorks **

RT Conference Proceedings

SR Electronic

ID 236253

A1 Owens, S.

A1 Myreen, Magnus O.

A1 Kumar, R.

A1 Tan, Y.K.

T1 Functional big-step semantics

YR 2016

T2 Lecture Notes in Computer Science; 25th European Symposium on Programming (ESOP)

SN 9783662494974

SP 589

OP 615

AB When doing an interactive proof about a piece of software, it is important that the underlying programming language’s semantics does not make the proof unnecessarily difficult or unwieldy. Both smallstep and big-step semantics are commonly used, and the latter is typically given by an inductively defined relation. In this paper, we consider an alternative: using a recursive function akin to an interpreter for the language. The advantages include a better induction theorem, less duplication, accessibility to ordinary functional programmers, and the ease of doing symbolic simulation in proofs via rewriting. We believe that this style of semantics is well suited for compiler verification, including proofs of divergence preservation. We do not claim the invention of this style of semantics: our contribution here is to clarify its value, and to explain how it supports several language features that might appear to require a relational or small-step approach. We illustrate the technique on a simple imperative language with C-like for-loops and a break statement, and compare it to a variety of other approaches. We also provide ML and lambda-calculus based examples to illustrate its generality.

LA eng

DO 10.1007/978-3-662-49498-1_23

LK http://dx.doi.org/10.1007/978-3-662-49498-1_23

OL 30