P.D. Mosses
info
Please Note
<p>This page displays the records of the person named above and is not linked to a unique person identifier. This record may need to be merged to a profile.</p>
9 records found
1
The Scheme programming language was introduced in 1975 as a lexically-scoped dialect of Lisp. It has subsequently been improved and extended through many rounds of standardization, documented by the Scheme Reports. In Lisp, eval is a function taking a single argument; when the value of the argument represents an expression, eval proceeds to evaluate it in the current environment. The Scheme procedure eval is similar, but takes an extra argument that determines the evaluation environment. The so-called classic standards for Scheme and its latest modern standard all include a denotational semantics of core expressions and of some required procedures. However, the semantics does not cover eval. When Muchnick and Pleban compared the denotational semantics of Lisp and Scheme in 1980, they wrote that it was not possible to give a structural semantics of eval expressions. Similarly, in 1984, Clinger pointed out that the semantics of eval violates compositionality; he suggested to define eval using a non-compositional copy of the semantic function. This paper adapts Clinger’s suggestion by letting the semantic function take an extra argument, then defining that argument by an explicit fixed point. The resulting semantics of eval expressions is fully compositional. The wellformedness of the semantics has been tested using a lightweight Agda formalization; verifying that the denotations have expected properties is work in progress.
...
The Scheme programming language was introduced in 1975 as a lexically-scoped dialect of Lisp. It has subsequently been improved and extended through many rounds of standardization, documented by the Scheme Reports. In Lisp, eval is a function taking a single argument; when the value of the argument represents an expression, eval proceeds to evaluate it in the current environment. The Scheme procedure eval is similar, but takes an extra argument that determines the evaluation environment. The so-called classic standards for Scheme and its latest modern standard all include a denotational semantics of core expressions and of some required procedures. However, the semantics does not cover eval. When Muchnick and Pleban compared the denotational semantics of Lisp and Scheme in 1980, they wrote that it was not possible to give a structural semantics of eval expressions. Similarly, in 1984, Clinger pointed out that the semantics of eval violates compositionality; he suggested to define eval using a non-compositional copy of the semantic function. This paper adapts Clinger’s suggestion by letting the semantic function take an extra argument, then defining that argument by an explicit fixed point. The resulting semantics of eval expressions is fully compositional. The wellformedness of the semantics has been tested using a lightweight Agda formalization; verifying that the denotations have expected properties is work in progress.
Jens Palsberg's first research publication was an OOPSLA '89 paper, coauthored with William Cook. In that much-cited paper, the authors identify self-reference as a central feature of inheritance, and analyze it using fixed points. They then define both an operational and a denotational semantics of inheritance, and prove them equivalent. Their proof exploits an intermediate semantics, obtained by step-indexing the operational semantics – an early use of the so-called 'fuel pattern'.
This paper presents an Agda formulation of the definitions and lemmas from the OOPSLA '89 paper. The Agda proof assistant detected some minor issues when type-checking the definitions; after they had been fixed, Agda successfully checked all the steps in the proofs of the lemmas. The Agda definitions and proofs make the same assumptions as the OOPSLA '89 paper about the existence of recursively defined Scott domains, and about the continuity of the defined functions. ...
This paper presents an Agda formulation of the definitions and lemmas from the OOPSLA '89 paper. The Agda proof assistant detected some minor issues when type-checking the definitions; after they had been fixed, Agda successfully checked all the steps in the proofs of the lemmas. The Agda definitions and proofs make the same assumptions as the OOPSLA '89 paper about the existence of recursively defined Scott domains, and about the continuity of the defined functions. ...
Jens Palsberg's first research publication was an OOPSLA '89 paper, coauthored with William Cook. In that much-cited paper, the authors identify self-reference as a central feature of inheritance, and analyze it using fixed points. They then define both an operational and a denotational semantics of inheritance, and prove them equivalent. Their proof exploits an intermediate semantics, obtained by step-indexing the operational semantics – an early use of the so-called 'fuel pattern'.
This paper presents an Agda formulation of the definitions and lemmas from the OOPSLA '89 paper. The Agda proof assistant detected some minor issues when type-checking the definitions; after they had been fixed, Agda successfully checked all the steps in the proofs of the lemmas. The Agda definitions and proofs make the same assumptions as the OOPSLA '89 paper about the existence of recursively defined Scott domains, and about the continuity of the defined functions.
This paper presents an Agda formulation of the definitions and lemmas from the OOPSLA '89 paper. The Agda proof assistant detected some minor issues when type-checking the definitions; after they had been fixed, Agda successfully checked all the steps in the proofs of the lemmas. The Agda definitions and proofs make the same assumptions as the OOPSLA '89 paper about the existence of recursively defined Scott domains, and about the continuity of the defined functions.
Software language design and implementation often involve specifications written in various esoteric meta-languages. Language workbenches generally include support for precise name-based navigation when browsing language specifications locally, but such support is lacking when browsing the same specifications online in code repositories.
This paper presents a technique to support precise name-based navigation of language specifications in online repositories using ordinary web browsers. The idea is to generate hyperlinked twins: websites where verbatim copies of specification text are enhanced with hyperlinks between name references and declarations. By generating hyperlinks directly from the name binding analysis used internally in a language workbench, online navigation in hyperlinked twins is automatically consistent with local navigation.
The presented technique has been implemented for the Spoofax language workbench, and used to generate hyperlinked twin websites from various language specifications in Spoofax meta-languages. However, the applicability of the technique is not limited to Spoofax, and developers of other language workbenches could presumably implement similar tooling, to make their language specifications more accessible to those who do not have the workbench installed.
...
Software language design and implementation often involve specifications written in various esoteric meta-languages. Language workbenches generally include support for precise name-based navigation when browsing language specifications locally, but such support is lacking when browsing the same specifications online in code repositories.
This paper presents a technique to support precise name-based navigation of language specifications in online repositories using ordinary web browsers. The idea is to generate hyperlinked twins: websites where verbatim copies of specification text are enhanced with hyperlinks between name references and declarations. By generating hyperlinks directly from the name binding analysis used internally in a language workbench, online navigation in hyperlinked twins is automatically consistent with local navigation.
The presented technique has been implemented for the Spoofax language workbench, and used to generate hyperlinked twin websites from various language specifications in Spoofax meta-languages. However, the applicability of the technique is not limited to Spoofax, and developers of other language workbenches could presumably implement similar tooling, to make their language specifications more accessible to those who do not have the workbench installed.
Spoofax is a language workbench. A Spoofax language specification generally includes name resolution: the analysis of bindings between definitions and references. When browsing code in the specified language using Spoofax, the bindings appear as hyperlinks, supporting precise name-based code navigation. However, Spoofax cannot be used for browsing code in online repositories. This paper is about a toolchain that uses Spoofax to generate hyperlinked twins of code repositories. These generated artefacts support the same precise code navigation as Spoofax, and can be browsed online. The technique has been prototyped on the CBS (Component-Based Semantics) specification language developed by the PLanCompS project, but could be used on any language after specifying its name resolution in Spoofax.
...
Spoofax is a language workbench. A Spoofax language specification generally includes name resolution: the analysis of bindings between definitions and references. When browsing code in the specified language using Spoofax, the bindings appear as hyperlinks, supporting precise name-based code navigation. However, Spoofax cannot be used for browsing code in online repositories. This paper is about a toolchain that uses Spoofax to generate hyperlinked twins of code repositories. These generated artefacts support the same precise code navigation as Spoofax, and can be browsed online. The technique has been prototyped on the CBS (Component-Based Semantics) specification language developed by the PLanCompS project, but could be used on any language after specifying its name resolution in Spoofax.
Specifying and mechanically verifying type safe programming languages requires significant effort. This effort can in theory be reduced by defining and reusing pre-verified, modular components. In practice, however, existing approaches to modular mechanical verification require many times as much specification code as plain, monolithic definitions. This makes it hard to develop new reusable components, and makes existing component specifications hard to grasp. We present an alternative approach based on intrinsically-typed interpreters, which reduces the size and complexity of modular specifications as compared to existing approaches. Furthermore, we introduce a new abstraction for safe-by-construction specification and composition of pre-verified type safe language components: language fragments. Language fragments are about as concise and easy to develop as plain, monolithic intrinsically-typed interpreters, but require about 10 times less code than previous approaches to modular mechanical verification of type safety.
...
Specifying and mechanically verifying type safe programming languages requires significant effort. This effort can in theory be reduced by defining and reusing pre-verified, modular components. In practice, however, existing approaches to modular mechanical verification require many times as much specification code as plain, monolithic definitions. This makes it hard to develop new reusable components, and makes existing component specifications hard to grasp. We present an alternative approach based on intrinsically-typed interpreters, which reduces the size and complexity of modular specifications as compared to existing approaches. Furthermore, we introduce a new abstraction for safe-by-construction specification and composition of pre-verified type safe language components: language fragments. Language fragments are about as concise and easy to develop as plain, monolithic intrinsically-typed interpreters, but require about 10 times less code than previous approaches to modular mechanical verification of type safety.
When a new programming language appears, the syntax and intended behaviour of its programs need to be specified. The behaviour of each language construct can be concisely specified by translating it to fundamental constructs (funcons), compositionally. In contrast to the informal explanations commonly found in reference manuals, such formal specifications of translations to funcons can be precise and complete. They are also easy to write and read, and to update when the language evolves. The PLanCompS project has developed a large collection of funcons. Each funcon is defined independently, using a modular variant of structural operational semantics. The definitions are available online, along with tools for generating funcon interpreters from them. This paper introduces and motivates funcons. It illustrates translation of language constructs to funcons, and funcon definition. It also relates funcons to the notation used in some previous language specification frameworks, including monadic semantics and action semantics.
...
When a new programming language appears, the syntax and intended behaviour of its programs need to be specified. The behaviour of each language construct can be concisely specified by translating it to fundamental constructs (funcons), compositionally. In contrast to the informal explanations commonly found in reference manuals, such formal specifications of translations to funcons can be precise and complete. They are also easy to write and read, and to update when the language evolves. The PLanCompS project has developed a large collection of funcons. Each funcon is defined independently, using a modular variant of structural operational semantics. The definitions are available online, along with tools for generating funcon interpreters from them. This paper introduces and motivates funcons. It illustrates translation of language constructs to funcons, and funcon definition. It also relates funcons to the notation used in some previous language specification frameworks, including monadic semantics and action semantics.
The CBS framework supports component-based specification of programming languages. It aims to significantly reduce the effort of formal language specification, and thereby encourage language developers to exploit formal semantics more widely. CBS provides an extensive library of reusable language specification components, facilitating co-evolution of languages and their specifications. After introducing CBS and its formal definition, this short paper reports work in progress on generating an IDE for CBS from the definition. It also considers the possibility of supporting component-based language specification in other formal language workbenches.
...
The CBS framework supports component-based specification of programming languages. It aims to significantly reduce the effort of formal language specification, and thereby encourage language developers to exploit formal semantics more widely. CBS provides an extensive library of reusable language specification components, facilitating co-evolution of languages and their specifications. After introducing CBS and its formal definition, this short paper reports work in progress on generating an IDE for CBS from the definition. It also considers the possibility of supporting component-based language specification in other formal language workbenches.
The SLE conference series is devoted to the engineering principles of software languages: their design, their implementation, and their evolution. This paper is about the role of language specification in SLE. A precise specification of a software language needs to be written in a formal meta-language, and it needs to co-evolve with the specified language. Moreover, different software languages often have features in common, which should provide opportunities for reuse of parts of language specifications. Support for co-evolution and reuse in a meta-language requires careful engineering of its design.
The author has been involved in the development of several meta-languages for semantic specification, including action semantics and modular variants of structural operational semantics (MSOS, I-MSOS). This led to the PLanCompS project, and to the design of its meta-language, CBS, for component-based semantics. CBS comes together with an extensible library of reusable components called ‘funcons’, corresponding to fundamental programming constructs. The main aim of CBS is to optimise co-evolution and reuse of specifications during language development, and to make specification of language semantics almost as straightforward as context-free syntax specification.
The paper discusses the engineering of a selection of previous meta-languages, assessing how well they support co-evolution and reuse. It then gives an introduction to CBS, and illustrates significant features. It also considers whether other current meta-languages might also be used to define an extensible library of funcons for use in component-based semantics. ...
The author has been involved in the development of several meta-languages for semantic specification, including action semantics and modular variants of structural operational semantics (MSOS, I-MSOS). This led to the PLanCompS project, and to the design of its meta-language, CBS, for component-based semantics. CBS comes together with an extensible library of reusable components called ‘funcons’, corresponding to fundamental programming constructs. The main aim of CBS is to optimise co-evolution and reuse of specifications during language development, and to make specification of language semantics almost as straightforward as context-free syntax specification.
The paper discusses the engineering of a selection of previous meta-languages, assessing how well they support co-evolution and reuse. It then gives an introduction to CBS, and illustrates significant features. It also considers whether other current meta-languages might also be used to define an extensible library of funcons for use in component-based semantics. ...
The SLE conference series is devoted to the engineering principles of software languages: their design, their implementation, and their evolution. This paper is about the role of language specification in SLE. A precise specification of a software language needs to be written in a formal meta-language, and it needs to co-evolve with the specified language. Moreover, different software languages often have features in common, which should provide opportunities for reuse of parts of language specifications. Support for co-evolution and reuse in a meta-language requires careful engineering of its design.
The author has been involved in the development of several meta-languages for semantic specification, including action semantics and modular variants of structural operational semantics (MSOS, I-MSOS). This led to the PLanCompS project, and to the design of its meta-language, CBS, for component-based semantics. CBS comes together with an extensible library of reusable components called ‘funcons’, corresponding to fundamental programming constructs. The main aim of CBS is to optimise co-evolution and reuse of specifications during language development, and to make specification of language semantics almost as straightforward as context-free syntax specification.
The paper discusses the engineering of a selection of previous meta-languages, assessing how well they support co-evolution and reuse. It then gives an introduction to CBS, and illustrates significant features. It also considers whether other current meta-languages might also be used to define an extensible library of funcons for use in component-based semantics.
The author has been involved in the development of several meta-languages for semantic specification, including action semantics and modular variants of structural operational semantics (MSOS, I-MSOS). This led to the PLanCompS project, and to the design of its meta-language, CBS, for component-based semantics. CBS comes together with an extensible library of reusable components called ‘funcons’, corresponding to fundamental programming constructs. The main aim of CBS is to optimise co-evolution and reuse of specifications during language development, and to make specification of language semantics almost as straightforward as context-free syntax specification.
The paper discusses the engineering of a selection of previous meta-languages, assessing how well they support co-evolution and reuse. It then gives an introduction to CBS, and illustrates significant features. It also considers whether other current meta-languages might also be used to define an extensible library of funcons for use in component-based semantics.
The potential benefits of formal semantics are well known. However, a substantial amount of work is required to produce a complete and accurate formal semantics for a major language; and when the language evolves, large-scale revision of the semantics may be needed to reflect the changes. The investment of effort needed to produce an initial definition, and subsequently to revise it, has discouraged language developers from using formal semantics. Consequently, many major programming languages (and most domain-specific languages) do not yet have formal semantic definitions. To improve the practicality of formal semantic definitions, the PLanCompS project has developed a component-based approach. In this approach, the semantics of a language is defined by translating its constructs (compositionally) to combinations of so-called fundamental constructs, or ‘funcons’. Each funcon is defined using a modular variant of Structural Operational Semantics, and forms a language-independent component that can be reused in definitions of different languages. A substantial library of funcons has been developed and tested in several case studies. Crucially, the definition of each funcon is fixed, and does not need changing when new funcons are added to the library. For specifying component-based semantics, we have designed and implemented a meta-language called CBS. It includes specification of abstract syntax, of its translation to funcons, and of the funcons themselves. Development of CBS specifications is supported by an integrated development environment. The accuracy of a language definition can be tested by executing the specified translation on programs written in the defined language, and then executing the resulting funcon terms using an interpreter generated from the CBS definitions of the funcons. This paper gives an introduction to CBS, illustrates its use, and presents the various tools involved in our implementation of CBS.
...
The potential benefits of formal semantics are well known. However, a substantial amount of work is required to produce a complete and accurate formal semantics for a major language; and when the language evolves, large-scale revision of the semantics may be needed to reflect the changes. The investment of effort needed to produce an initial definition, and subsequently to revise it, has discouraged language developers from using formal semantics. Consequently, many major programming languages (and most domain-specific languages) do not yet have formal semantic definitions. To improve the practicality of formal semantic definitions, the PLanCompS project has developed a component-based approach. In this approach, the semantics of a language is defined by translating its constructs (compositionally) to combinations of so-called fundamental constructs, or ‘funcons’. Each funcon is defined using a modular variant of Structural Operational Semantics, and forms a language-independent component that can be reused in definitions of different languages. A substantial library of funcons has been developed and tested in several case studies. Crucially, the definition of each funcon is fixed, and does not need changing when new funcons are added to the library. For specifying component-based semantics, we have designed and implemented a meta-language called CBS. It includes specification of abstract syntax, of its translation to funcons, and of the funcons themselves. Development of CBS specifications is supported by an integrated development environment. The accuracy of a language definition can be tested by executing the specified translation on programs written in the defined language, and then executing the resulting funcon terms using an interpreter generated from the CBS definitions of the funcons. This paper gives an introduction to CBS, illustrates its use, and presents the various tools involved in our implementation of CBS.