jana/eelco-visser-compiler-construction
1
0
Fork 0
Code Issues Pull requests Projects Releases Packages Wiki Activity Actions
eelco-visser-compiler-const.../lecture/7.html

1039 lines
19 KiB
HTML
Raw Permalink Blame History

This file contains ambiguous Unicode characters

This file contains Unicode characters that might be confused with other characters. If you think that this is intentional, you can safely ignore this warning. Use the Escape button to reveal them.

<!doctype html>
<html lang="en">
<head>
<meta charset="utf-8">
<meta name="viewport" content="width=device-width, initial-scale=1, shrink-to-fit=no">
<meta name="description" content="">
<meta name="author" content="Eelco Visser">
<meta name="generator" content="Jekyll v3.8.5">
<title>Lecture 7: More Constraints and Statix</title>
<!-- <base href="/2021"> -->
<!--link rel="canonical" href="https://getbootstrap.com/docs/4.3/examples/starter-template/"-->
<link rel="icon" href="../img/logo/pl_ico2_2B3_icon.ico" type="image/x-icon">
<!-- Bootstrap core CSS -->
<!--link href="https://getbootstrap.com/docs/4.3/dist/css/bootstrap.min.css" rel="stylesheet" integrity="sha384-ggOyR0iXCbMQv3Xipma34MD+dH/1fQ784/j6cY/iJTQUOhcWr7x9JvoRxT2MZw1T" crossorigin="anonymous"-->
<link rel="stylesheet" href="https://stackpath.bootstrapcdn.com/bootstrap/4.3.1/css/bootstrap.min.css" integrity="sha384-ggOyR0iXCbMQv3Xipma34MD+dH/1fQ784/j6cY/iJTQUOhcWr7x9JvoRxT2MZw1T" crossorigin="anonymous">
<style>
.bd-placeholder-img {
font-size: 1.125rem;
text-anchor: middle;
-webkit-user-select: none;
-moz-user-select: none;
-ms-user-select: none;
user-select: none;
}
@media (min-width: 768px) {
.bd-placeholder-img-lg {
font-size: 3.5rem;
}
}
</style>
<!-- Custom styles for this template -->
<link href="../css/main.css" rel="stylesheet">
<link href="../css/borders-responsive.css" rel="stylesheet">
<link rel="stylesheet" href="../css/pl.css">
</head>
<body>
<nav class="navbar navbar-expand-md navbar-dark bg-dark fixed-top">
<a class="navbar-brand" href="../index.html">
TU Delft | CS4200
</a>
<button class="navbar-toggler" type="button" data-toggle="collapse" data-target="#navbarsExampleDefault" aria-controls="navbarsExampleDefault" aria-expanded="false" aria-label="Toggle navigation">
<span class="navbar-toggler-icon"></span>
</button>
<div class="collapse navbar-collapse" id="navbarsExampleDefault">
<ul class="navbar-nav mr-auto">
<li class="nav-item active">
<a class="nav-link" href="../lectures/index.html" tabindex="-1" aria-disabled="true">Lectures</a>
</li>
<li class="nav-item active">
<a class="nav-link" href="../homework/index.html" tabindex="-1" aria-disabled="true">Homework</a>
</li>
<li class="nav-item active">
<a class="nav-link" href="../project/index.html" tabindex="-1" aria-disabled="true">Project</a>
</li>
<li class="nav-item active">
<a class="nav-link" href="../news/index.html" tabindex="-1" aria-disabled="true">News</a>
</li>
<li class="nav-item active">
<a class="nav-link" href="../blog/index.html" tabindex="-1" aria-disabled="true">Blog</a>
</li>
</ul>
</div>
</nav>
<div class="container">
<div class="row">
<div class="col-sm-12 col-md-12 col-lg-12 col-xl-12">
<div class="mt-3 mb-3 pt-3 pb-3 text-dark border-top border-bottom border-grey">
<div class="text-dark font-weight-bold">
<h1>
Lecture 7: More Constraints and Statix
</h1>
</div>
<div>
Eelco Visser
</div>
<div>
Lecture
</div>
<div>
October 07, 2021
</div>
</div>
</div>
</div>
<div class="row">
<div class="col-sm-12 col-md-12 col-lg-9 border-lg-right border-grey">
<p>In this lecture we discuss material we didn’t get to in the previous two lectures.</p>
<h3 id="references">References</h3>
<ul class="list-group list-group-flush pb-3">
<li class="list-group-item pl-lg-0 border-0 pb-0">
<div class="bd-callout border-danger pl-3">
<div>
<a name="RouvoetAPKV20"></a>
<a class="font-weight-bold text-dark" target="_blank" href="https://doi.org/10.1145/3428248">Knowing when to ask: sound scheduling of name resolution in type checkers derived from declarative specifications</a>
</div>
<div class="font-weight-light text-secondary" style="font-size:90%;">
<a class="text-secondary" href="https://www.linkedin.com/in/arjen-rouvoet-760347a5/">Arjen Rouvoet</a>, <a class="text-secondary" href="https://researchr.org/alias/hendrik-van-antwerpen">Hendrik van Antwerpen</a>, <a class="text-secondary" href="http://www.casperbp.net">Casper Bach Poulsen</a>, <a class="text-secondary" href="https://researchr.org/alias/robbert-krebbers">Robbert Krebbers</a>, <a class="text-secondary" href="http://eelcovisser.org">Eelco Visser</a>.
</div>
<div class="font-weight-light text-secondary" style="font-size:90%;">
PACMPL 4(OOPSLA) 2020
[<a href="../publications/2020/RouvoetAPKV20.pdf" class="text-secondary" target="_blank">pdf</a>, <a class="text-secondary" href="https://doi.org/10.1145/3428248" target="_blank">doi</a>, <a class="text-secondary" target="_blank" href="https://researchr.org/publication/RouvoetAPKV20/bibtex">bib</a>, <a href="https://researchr.org/publication/RouvoetAPKV20" class="text-secondary" target="_blank">researchr</a>, <a class="text-secondary" data-toggle="collapse" href="7.html#AbstractRouvoetAPKV20" role="button" aria-expanded="false" aria-controls="AbstractRouvoetAPKV20"">abstract</a>]
<!-- -->
</div>
<div class="collapse mt-1 mb-2" id="AbstractRouvoetAPKV20">
<div class="">
There is a large gap between the specification of type systems and the implementation of their type checkers, which impedes reasoning about the soundness of the type checker with respect to the specification. A vision to close this gap is to automatically obtain type checkers from declarative programming language specifications. This moves the burden of proving correctness from a case-by-case basis for concrete languages to a single correctness proof for the specification language. This vision is obstructed by an aspect common to all programming languages: name resolution. Naming and scoping are pervasive and complex aspects of the static semantics of programming languages. Implementations of type checkers for languages with name binding features such as modules, imports, classes, and inheritance interleave collection of binding information (i.e., declarations, scoping structure, and imports) and querying that information. This requires scheduling those two aspects in such a way that query answers are stable—i.e., they are computed only after all relevant binding structure has been collected. Type checkers for concrete languages accomplish stability using language-specific knowledge about the type system. In this paper we give a language-independent characterization of necessary and sufficient conditions to guarantee stability of name and type queries during type checking in terms of critical edges in an incomplete scope graph. We use critical edges to give a formal small-step operational semantics to a declarative specification language for type systems, that achieves soundness by delaying queries that may depend on missing information. This yields type checkers for the specified languages that are sound by construction—i.e., they schedule queries so that the answers are stable, and only accept programs that are name- and type-correct according to the declarative language specification. We implement this approach, and evaluate it against specifications of a small module and record language, as well as subsets of Java and Scala.
</div>
</div>
</div>
</li>
<li class="list-group-item pl-lg-0 border-0 pb-0">
<div class="bd-callout border-danger pl-3">
<div>
<a name="AntwerpenPRV18"></a>
<a class="font-weight-bold text-dark" target="_blank" href="https://doi.org/10.1145/3276484">Scopes as types</a>
</div>
<div class="font-weight-light text-secondary" style="font-size:90%;">
<a class="text-secondary" href="https://nl.linkedin.com/in/hendrikvanantwerpen">Hendrik van Antwerpen</a>, <a class="text-secondary" href="http://www.casperbp.net">Casper Bach Poulsen</a>, <a class="text-secondary" href="https://www.linkedin.com/in/arjen-rouvoet-760347a5/">Arjen Rouvoet</a>, <a class="text-secondary" href="http://eelcovisser.org">Eelco Visser</a>.
</div>
<div class="font-weight-light text-secondary" style="font-size:90%;">
PACMPL 2(OOPSLA) 2018
[<a href="../publications/2018/AntwerpenPRV18.pdf" class="text-secondary" target="_blank">pdf</a>, <a class="text-secondary" href="https://doi.org/10.1145/3276484" target="_blank">doi</a>, <a class="text-secondary" target="_blank" href="https://researchr.org/publication/AntwerpenPRV18/bibtex">bib</a>, <a href="https://researchr.org/publication/AntwerpenPRV18" class="text-secondary" target="_blank">researchr</a>, <a class="text-secondary" data-toggle="collapse" href="7.html#AbstractAntwerpenPRV18" role="button" aria-expanded="false" aria-controls="AbstractAntwerpenPRV18"">abstract</a>]
<!-- -->
</div>
<div class="collapse mt-1 mb-2" id="AbstractAntwerpenPRV18">
<div class="">
Scope graphs are a promising generic framework to model the binding structures of programming languages, bridging formalization and implementation, supporting the definition of type checkers and the automation of type safety proofs. However, previous work on scope graphs has been limited to simple, nominal type systems. In this paper, we show that viewing scopes as types enables us to model the internal structure of types in a range of non-simple type systems (including structural records and generic classes) using the generic representation of scopes. Further, we show that relations between such types can be expressed in terms of generalized scope graph queries. We extend scope graphs with scoped relations and queries. We introduce Statix, a new domain-specific meta-language for the specification of static semantics, based on scope graphs and constraints. We evaluate the scopes as types approach and the Statix design in case studies of the simply-typed lambda calculus with records, System F, and Featherweight Generic Java.
</div>
</div>
</div>
</li>
<li class="list-group-item pl-lg-0 border-0 pb-0">
<div class="bd-callout border-primary pl-3">
<div>
<a name="AntwerpenNTVW16"></a>
<a class="font-weight-bold text-dark" target="_blank" href="http://doi.acm.org/10.1145/2847538.2847543">A constraint language for static semantic analysis based on scope graphs</a>
</div>
<div class="font-weight-light text-secondary" style="font-size:90%;">
<a class="text-secondary" href="https://nl.linkedin.com/in/hendrikvanantwerpen">Hendrik van Antwerpen</a>, <a class="text-secondary" href="https://researchr.org/profile/pierrejeanmichelneron/publications">Pierre Néron</a>, <a class="text-secondary" href="http://www.cs.pdx.edu/~apt">Andrew P. Tolmach</a>, <a class="text-secondary" href="http://eelcovisser.org">Eelco Visser</a>, <a class="text-secondary" href="https://www.linkedin.com/in/guidowachsmuth/">Guido Wachsmuth</a>.
</div>
<div class="font-weight-light text-secondary" style="font-size:90%;">
PEPM 2016
[<a href="../publications/2016/AntwerpenNTVW16.pdf" class="text-secondary" target="_blank">pdf</a>, <a class="text-secondary" href="http://doi.acm.org/10.1145/2847538.2847543" target="_blank">doi</a>, <a class="text-secondary" target="_blank" href="https://researchr.org/publication/AntwerpenNTVW16/bibtex">bib</a>, <a href="https://researchr.org/publication/AntwerpenNTVW16" class="text-secondary" target="_blank">researchr</a>, <a class="text-secondary" data-toggle="collapse" href="7.html#AbstractAntwerpenNTVW16" role="button" aria-expanded="false" aria-controls="AbstractAntwerpenNTVW16"">abstract</a>]
<!-- -->
</div>
<div class="collapse mt-1 mb-2" id="AbstractAntwerpenNTVW16">
<div class="">
In previous work, we introduced scope graphs as a formalism for describing program binding structure and performing name resolution in an AST-independent way. In this paper, we show how to use scope graphs to build static semantic analyzers. We use constraints extracted from the AST to specify facts about binding, typing, and initialization. We treat name and type resolution as separate building blocks, but our approach can handle language constructs -- such as record field access -- for which binding and typing are mutually dependent. We also refine and extend our previous scope graph theory to address practical concerns including ambiguity checking and support for a wider range of scope relationships. We describe the details of constraint generation for a model language that illustrates many of the interesting static analysis issues associated with modules and records.
</div>
</div>
</div>
</li>
<li class="list-group-item pl-lg-0 border-0 pb-0">
<div class="bd-callout border-primary pl-3">
<div>
<a name="NeronTVW15"></a>
<a class="font-weight-bold text-dark" target="_blank" href="http://dx.doi.org/10.1007/978-3-662-46669-8\_9">A Theory of Name Resolution</a>
</div>
<div class="font-weight-light text-secondary" style="font-size:90%;">
<a class="text-secondary" href="https://researchr.org/profile/pierrejeanmichelneron/publications">Pierre Néron</a>, <a class="text-secondary" href="http://www.cs.pdx.edu/~apt">Andrew P. Tolmach</a>, <a class="text-secondary" href="http://eelcovisser.org">Eelco Visser</a>, <a class="text-secondary" href="https://www.linkedin.com/in/guidowachsmuth/">Guido Wachsmuth</a>.
</div>
<div class="font-weight-light text-secondary" style="font-size:90%;">
ESOP 2015
[<a href="../publications/2015/NeronTVW15.pdf" class="text-secondary" target="_blank">pdf</a>, <a class="text-secondary" href="http://dx.doi.org/10.1007/978-3-662-46669-8\_9" target="_blank">doi</a>, <a class="text-secondary" target="_blank" href="https://researchr.org/publication/NeronTVW15/bibtex">bib</a>, <a href="https://researchr.org/publication/NeronTVW15" class="text-secondary" target="_blank">researchr</a>, <a class="text-secondary" data-toggle="collapse" href="7.html#AbstractNeronTVW15" role="button" aria-expanded="false" aria-controls="AbstractNeronTVW15"">abstract</a>]
<!-- -->
</div>
<div class="collapse mt-1 mb-2" id="AbstractNeronTVW15">
<div class="">
We describe a language-independent theory for name binding and resolution, suitable for programming languages with complex scoping rules including both lexical scoping and modules. We formulate name resolution as a two-stage problem. First a language-independent scope graph is constructed using language-specific rules from an abstract syntax tree. Then references in the scope graph are resolved to corresponding declarations using a language-independent resolution process. We introduce a resolution calculus as a concise, declarative, and languageindependent specification of name resolution. We develop a resolution algorithm that is sound and complete with respect to the calculus. Based on the resolution calculus we develop language-independent definitions of α-equivalence and rename refactoring. We illustrate the approach using a small example language with modules. In addition, we show how our approach provides a model for a range of name binding patterns in existing languages.
</div>
</div>
</div>
</li>
<li class="list-group-item pl-lg-0 border-0 pb-0">
<div class="bd-callout border-primary pl-3">
<div>
<a name="BaaderS01"></a>
Unification Theory
</div>
<div class="font-weight-light text-secondary" style="font-size:90%;">
<a class="text-secondary" href="https://researchr.org/alias/franz-baader">Franz Baader</a>, <a class="text-secondary" href="https://researchr.org/alias/wayne-snyder">Wayne Snyder</a>.
</div>
<div class="font-weight-light text-secondary" style="font-size:90%;">
Handbook of Automated Reasoning (in 2 volumes) 2001
[<a class="text-secondary" target="_blank" href="https://researchr.org/publication/BaaderS01/bibtex">bib</a>, <a href="https://researchr.org/publication/BaaderS01" class="text-secondary" target="_blank">researchr</a>]
<!-- BaaderS01 -->
</div>
</div>
</li>
</ul>
</div>
<div class="col-sm-12 col-md-12 col-lg-3 col-xl-3 " >
<div class="sticky-top top70 d-none d-lg-block d-xl-block">
<div class="pb4 mb3 border-bottom border-grey ">
<nav>
<ul class="pagination justify-content-left">
<li class="page-item">
<a class="page-link" href="6.html">
&laquo;
</a>
</li>
<li class="page-item">
<a class="page-link" href="../lectures/index.html">
^
</a>
</li>
<li class="page-item">
<a class="page-link" href="8.html">&raquo;</a>
</li>
</ul>
</nav>
</div>
<ul id="my_toc" class="toc list-group list-group-flush d-none d-lg-block d-xl-block p-0 ml-0 mt-3">
<li class="list-group-item pl-0 ml-0 border-0 pl-0 pt-0 pb-1 pr-0 m-0 mr-3"><a href="7.html#references">References</a></li>
</ul>
</div>
</div>
</div>
<div class="row">
<div class="col-12">
<div class="border-top border-bottom border-grey mt-3 pt-3">
<nav>
<ul class="pagination justify-content-center">
<li class="page-item">
<a class="page-link" href="6.html">
Previous
</a>
</li>
<li class="page-item">
<a class="page-link" href="8.html">Next</a>
</li>
<li class="page-item">
<a class="page-link" href="../lectures/index.html">
Index
</a>
</li>
</ul>
</nav>
</div>
</div>
</div>
</div>
<!-- Optional JavaScript -->
<!-- jQuery first, then Popper.js, then Bootstrap JS -->
<script src="https://code.jquery.com/jquery-3.3.1.slim.min.js" integrity="sha384-q8i/X+965DzO0rT7abK41JStQIAqVgRVzpbzo5smXKp4YfRvH+8abtTE1Pi6jizo" crossorigin="anonymous"></script>
<script src="https://cdnjs.cloudflare.com/ajax/libs/popper.js/1.14.7/umd/popper.min.js" integrity="sha384-UO2eT0CpHqdSJQ6hJty5KVphtPhzWj9WO1clHTMGa3JDZwrnQq4sF86dIHNDz0W1" crossorigin="anonymous"></script>
<script src="https://stackpath.bootstrapcdn.com/bootstrap/4.3.1/js/bootstrap.min.js" integrity="sha384-JjSmVgyd0p3pXB1rRibZUAYoIIy6OrQ6VrjIEaFf/nJGzIxFDsf4x0xIM+B07jRM" crossorigin="anonymous"></script>
</body>
</html>
Reference in a new issue View git blame Copy permalink