Tutorials

Gradual typing enables the smooth integration of static and dynamic typechecking. In this tutorial, we will review the core concepts of gradual typing, informed by a formal framework to derive the semantics of a gradually-typed language from a statically-typed counterpart. We will then discuss some applications of gradual typing to challenging typing disciplines.

Static type systems are an excellent light-weight tool to improve code quality. Every compile your program is checked so that interfaces between parts of your system are verified to be correct, and depending on how strong the type system is, many important invariants are verified quickly and soundly. In this tutorial I shall discuss how to set up a static type system for a functional language and we shall be looking at Damas-Milner’s algorithm W for performing the inference. We shall then look at how you can implement a static analysis on top of a a type system, taking advantage of the underlying type system’s implementation. No knowledge of functional programming is assumed, but it can be helpful.

Formal Languages and Automata Theory (FLAT) courses present challenges for both the students and the instructors. Many students dislike such a course given the mathematical and theoretical nature of the topics as well as the formal notation used. In many cases, this leads to apathy among Computer Science students that enjoy and prefer programming courses. In turn, this presents a problem for instructors that frequently struggle to motivate their students to master the material. To address poor motivation and apathy, many FLAT instructors turn to constructivism to formulate classroom strategies and pedagogic tools. Constructivism is a theory of learning that postulates that knowledge is not passively absorbed through lectures and textbooks and, instead, knowledge is actively constructed by students engaged in building activities such as designing and implementing programs. A modern trend in FLAT education adopts a programming-based methodology to deliver FLAT courses. This tutorial illustrates how to deliver a programming-based course using FSM (Functional State Machines). FSM is a domain-specific language embedded in Racket that provides the programmer with the ability to design, implement, test, and verify state-based machines, grammars, regular expressions, and associated algorithms typically developed as part of the constructive proofs students are exposed to in a FLAT course. FSM is tightly coupled with a powerful suite of visualization tools and the textbook, Programming-Based Formal Languages and Automata Theory, that presents design recipes for the implementation of machines, grammars, and regular expressions. The tutorial focuses on how FSM may be used in the FLAT classroom without sacrificing content or rigor.
To fully participate in hands-on exercises participants ought to install on their machines, prior to the tutorial, the following software:

• DrRacket: https://download.racket-lang.org/
• GraphViz: https://github.com/morazanm/fsm/blob/master/fsm-gviz/README.md
• FSM: https://github.com/morazanm/fsm/blob/master/fsm-docs/readmes/fsm_install.md