Browsing by Subject "programming languages"

Now showing 1 - 2 of 2
  • Thumbnail Image
    Item
    Modular metatheory for extensible languages
    (2024-08) Michaelson, Dawn
    The features available in a programming language affect how easy it is to write programs for different purposes using it. Extensible languages allow specifications of language features to be developed independently of one another, then composed to form a new language containing all the features from all the specifications included. This lets programmers choose language features they find useful for each program they write. However, because the specifications of different language features are developed independently of one another, we do not know the language resulting from composition is well-formed in desired ways. In particular, we don’t know what properties should be true of the language, nor do we have a proof that they are true; that is, we do not have metatheory, a set of properties proven to be true, for the language. Metatheoretic properties are known to hold for any program written in the language, providing useful information to programmers about what can and cannot happen in a program. For example, the type preservation property can be stated as terms with a certain type evaluate to values of the same type, and guarantees well-typed programs cannot encounter type errors during evaluation. In an extensible setting, proving properties will hold for any composed language is difficult because the full language is not created until the time of composition. This thesis develops a modular approach to establishing the metatheory of extensible languages written using a framework where modules specifying language features may build on others. In this approach, each specification module independently introduces new metatheoretic properties expected to hold for any composed language that includes the module. The work of proving these properties for any composed language is distributed across modules, with each module contributing proofs for the new properties it introduces and those of the modules on which it builds. These proofs are written in the limited context of a single module’s knowledge but need to reason about the larger contexts of composed languages, which may include constructs unknown to the module writing the proof. To address this, we utilize generic reasoning to handle the currently-unknown additions that may be present in a composed language. When a language composition is built, the proofs from each module are then used to create a composed proof for each property. These composed proofs guarantee each property from each module included in the composition holds for the composed language, bringing the benefits of metatheory to the extensible setting. In addition to developing a reasoning framework for modular metatheory, we implement it in an interactive proof assistant named Extensibella. Extensibella aids users in writing modular proofs. It does this by adding an extra layer to Abella, an existing proof assistant. This extra layer checks the proofs are valid in the context of a single module and that generic reasoning is carried out correctly, then passes proofs to Abella to check their validity in the logic G in which it constructs proofs. Extensibella also includes functionality to compose the proofs from individual modules to form full proofs of properties for any composed language. To support this implementation, we have also implemented the framework for language specification about which we reason in a system named Sterling. Sterling allows users to write language specifications and check them for their modular validity, then produces specifications Extensibella can read and about which it can reason. Finally, using these implementations, we have developed a set of example extensible languages and their metatheory. These applications suggest our framework’s structure does not induce significant limits on what we can prove, so modules can introduce interesting new syntax, semantics, and metatheoretic properties. They also allow us to examine the trade offs in our framework between the freedom given to modules to introduce interesting new syntax and semantics and the ability to introduce and prove new metatheoretic properties.
  • Thumbnail Image
    Item
    Oral History with Kurt Maly
    (Charles Babbage Institute, 2020-12-03) Maly, Kurt
    This interview was conducted by CBI for CS&E in conjunction with the 50th Anniversary of the University of Minnesota Computer Science Department (now Computer Science and Engineering, CS&E). The first part of the interview Professor Maly discusses his education in Vienna before his doctoral work at the Courant Institute at New York University working under Jack Schwartz, and the dissertation he wrote on the programming language SETL. He joined the newly formed Computer Science Department at the University of Minnesota in the early 1970s and in 1974 became the Director of Undergraduate Education for the department. After promotion to Associate Professor, he became the Department Chair. In the oral history, he discusses the early faculty member of the department such as Marvin Stein, Bill Munro, Jay Leavitt, Bill Franta, Ben Rosen, and others. Among other topics he explores are the Computer Center and its equipment, collaborating with industry to enhance resources and facilities, the early curriculum, early lessons and continuing leadership as Department Chair, serving on the board of the Microelectronics Institute (MEIC). He also highlights the early and continuing impact of the Cray Lectureship for some world-renowned computer scientists to come to the department for a short stretch to give a number of talks and interact with faculty and students. Early lecturers included Barry Boehm, Nikolas Wirth, and other computer top scientists. At Minnesota, he was learning the ropes of being Chair as rank junior to full professor in the department. Having successfully led the Department of CS to a very strong if not elite level, he decided to take on the challenge of building a program up in both research and education at Old Dominion (when he arrived it had no significant research profile). He chaired the department for many years and formed strong partnerships in the region with William Wulf and Anita Jones at Virginia, and schools in the DC area as well as with NSF.