@techreport{
    tPreoteasa04a,
    author = "Preoteasa, Viorel",
    isbn = "952-12-1319-1",
    title = "Refinement of Recursive Procedures with Parameters in {PVS}",
    abstract = "We present a shallow embedding in PVS of a predicate transformer semantics of an imperative language suitable for reasoning about recursive procedures with parameters and local variables. We use the PVS dependent type mech- anism for implementing program variables of different types. We use an un- interpreted state space and define the program variables behavior by means of certain tree functions that are supposed to satisfy some axioms. Unlike in the implementations mentioned in the literature, we do not need to change the state space when adding local variables or procedure parameters.",
    year = "2004",
    number = "596",
    lab = "Software Construction",
    month = "Mar",
    flags = "copy",
    address = "Turku, Finland",
    pdf = "TR596.pdf",
    institution = "{TUCS} - Turku Centre for Computer Science"
}