אירועים והרצאות בפקולטה למדעי המחשב ע"ש הנרי ומרילין טאוב

Modern programming languages rely on advanced and intricate type systems.
Expressive type systems support more language features but often result in unexpected language capabilities. For example, we know that the Java type system is Turing complete, which means it is so complex that Java compilers cannot guarantee termination. But a powerful type system can also be a blessing in disguise. Over the years, crafty programmers found ways to coerce type systems to perform basic computations at the type level. Certain program interfaces employ this form of metaprogramming to detect and report specialized program bugs before runtime.

In classical computer science, the notion of computational power is tightly coupled with automata (abstract machines) such as finite-state and Turing machines. We reason about the computability of various type systems by connecting them with well-founded classes of automata through type automata -- machines that employ program types as control and storage. By describing a bisimulation between type automata and classical automata, we precisely classify the expressiveness of a type system.

This work is comprised of a series of studies that analyze different type systems using type automata. We classify the computability of the decidable type systems fragments of Kennedy and Pierce in terms of regular and context-free tree languages. On the other hand, we prove that the Python type system defined in PEP 484 is Turing complete. In addition, we introduce novel metaprogramming techniques for an advanced interface design called fluent API. Our fluent APIs can enforce the API protocol or the grammar of an embedded domain-specific language (DSL) at compile time. We present the first fluent API design that supports all deterministic context-free API protocols and DSLs. We also demonstrate how to create elegant and sophisticated fluent APIs in functional programming languages.