626 research outputs found
Renamingless Capture-Avoiding Substitution for Definitional Interpreters
Full text linkSubstitution is a common and popular approach to implementing name binding in definitional interpreters. A common pitfall of implementing substitution functions is variable capture. The traditional approach to avoiding variable capture is to rename variables. However, traditional renaming makes for an inefficient interpretation strategy. Furthermore, for applications where partially-interpreted terms are user facing it can be confusing if names in uninterpreted parts of the program have been changed. In this paper we explore two techniques for implementing capture avoiding substitution in definitional interpreters to avoid renaming
Allisyn Casper Family History
Full text linkAllisyn Brielle Casper authored this family history as part of the course requirements for HIST 550/700 Your Family in History offered online in Fall 2019 and was submitted to the Pittsburg State University Digital Commons. Please contact the author directly with any questions or comments: [email protected]
Defining Name Accessibility Using Scope Graphs (Artifact)
Full text linkMany programming languages allow programmers to regulate accessibility; i.e., annotating a declaration with keywords such as export and private to indicate where it can be accessed. Despite the importance of name accessibility for, e.g., compilers, editor auto-completion and tooling, and automated refactorings, few existing type systems provide a formal account of name accessibility.
We present a declarative, executable, and language-parametric model for name accessibility, which provides a formal specification of name accessibility in Java, C#, C++, Rust, and Eiffel. We achieve this by defining name accessibility as a predicate on resolution paths through scope graphs. Since scope graphs are a language-independent model of name resolution, our model provides a uniform approach to defining different accessibility policies for different languages.
Our model is implemented in Statix, a logic language for executable type system specification using scope graphs. We evaluate its correctness on a test suite that compares it with the C#, Java, and Rust compilers, and show we can synthesize access modifiers in programs with holes accurately
Defining Name Accessibility Using Scope Graphs
Full text linkMany programming languages allow programmers to regulate accessibility; i.e., annotating a declaration with keywords such as export and private to indicate where it can be accessed. Despite the importance of name accessibility for, e.g., compilers, editor auto-completion and tooling, and automated refactorings, few existing type systems provide a formal account of name accessibility.
We present a declarative, executable, and language-parametric model for name accessibility, which provides a formal specification of name accessibility in Java, C#, C++, Rust, and Eiffel. We achieve this by defining name accessibility as a predicate on resolution paths through scope graphs. Since scope graphs are a language-independent model of name resolution, our model provides a uniform approach to defining different accessibility policies for different languages.
Our model is implemented in Statix, a logic language for executable type system specification using scope graphs. We evaluate its correctness on a test suite that compares it with the C#, Java, and Rust compilers, and show we can synthesize access modifiers in programs with holes accurately
Mophasco (MOnadic framework for PHAsed name resolution using SCOpe graphs)
No full textArtifact accompanying paper
Casper Bach Poulsen, Aron Zwaan, Paul Hübner. 2023. “A Monadic Framework for Name Resolution in Multi-Phased Type Checkers”. In Proceedings of the 22nd ACM SIGPLAN International Conference on Generative Programming: Concepts and Experiences (GPCE '23), October 22--23, 2023, Cascais, Portugal. https://doi.org/10.1145/3624007.3624051
For more details, see the included READM
Casper the Friendly Ghost: Far-Out Fables
No full text"As I fully expected, this paperback book has nothing to do with Aesopic fables. It contains standard Casper cartoon stories. I read the first, "Every Litter Bit Helps." It is rather a full story, lasting 42 pages. In typical cartoon style, it brings together contemporary concerns like littering; traditional views of fascinating things like witches and ghosts; evil characters and good characters -- Casper and his friend, Wendy, the good little witch; and happy endings. Keeping it in the collection may help some future researcher to know what kind of book it is."No Autho
Freight Lubricating Oil from North of Casper, Wyo.
No full textFreight Lubricating Oil from North of Casper, Wyo
Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics (Artifact)
Full text linkOur paper introduces a systematic approach to the alignment of names in the static structure of a program, and memory layout and access during its execution. We develop a uniform memory model consisting of frames that instantiate the scopes in the scope graph of a program. This provides a language-independent correspondence between static scopes and run-time memory layout, and between static resolution paths and run-time memory access paths. The approach scales to a range of binding features, supports straightforward type soundness proofs, and provides the basis for a language-independent specification of sound reachability-based garbage collection.
This Coq artifact showcases how our uniform model for memory layout in dynamic semantics provides structure to type soundness proofs. The artifact contains type soundness proofs mechanized in Coq for (supersets of) all languages in the paper. The type soundness proofs rely on a language-independent framework formalizing scope graphs and frame heaps
Scopes Describe Frames: A Uniform Model for Memory Layout in Dynamic Semantics
Full text linkSemantic specifications do not make a systematic connection between the names and scopes in the static structure of a program and memory layout, and access during its execution. In this paper, we introduce a systematic approach to the alignment of names in static semantics and memory in dynamic semantics, building on the scope graph framework for name resolution. We develop a uniform memory model consisting of frames that instantiate the scopes in the scope graph of a program. This provides a language-independent correspondence between static scopes and run-time memory layout, and between static resolution paths and run-time memory access paths. The approach scales to a range of binding features, supports straightforward type soundness proofs, and provides the basis for a language-independent specification of sound reachability-based garbage collection
- …
