Subscribe to the gold package and get unlimited access to Shamra Academy
Register a new userDependent Type Systems as Macros
86
0
0.0
(
0
)
Added by
William J. Bowman
Publication date
2021
fields
Informatics Engineering
and research's language is
English
Ask ChatGPT about the research
No Arabic abstract
We present Turnstile+, a high-level, macros-based metaDSL for building dependently typed languages. With it, programmers may rapidly prototype and iterate on the design of new dependently typed features and extensions. Or they may create entirely new DSLs whose dependent type power is tailored to a specific domain. Our frameworks support of language-oriented programming also makes it suitable for experimenting with systems of interacting components, e.g., a proof assistant and its companion DSLs. This paper explains the implementation details of Turnstile+, as well as how it may be used to create a wide-variety of dependently typed languages, from a lightweight one with indexed types, to a full spectrum proof assistant, complete with a tactic system and extensions for features like sized types and SMT interaction.
rate research
Read More
We show canonicity and normalization for dependent type theory with a cumulative sequence of universes and a type of Boolean. The argument follows the usual notion of reducibility, going back to Godels Dialectica interpretation and the work of Tait. A key feature of our approach is the use of a proof relevant notion of reducibility.
We present a domain-independent algorithm that computes macros in a novel way. Our algorithm computes macros on-the-fly for a given set of states and does not require previously learned or inferred information, nor prior domain knowledge. The algorithm is used to define new domain-independent tractable classes of classical planning that are proved to include emph{Blocksworld-arm} and emph{Towers of Hanoi}.
Multitier programming languages reduce the complexity of developing distributed systems by developing the distributed system in a single coherent code base. The compiler or the runtime separate the code for the components of the distributed system, enabling abstraction over low level implementation details such as data representation, serialization and network protocols. Our ScalaLoci language allows developers to declare the different components and their architectural relation at the type level, allowing static reasoning about about distribution and remote communication and guaranteeing static type safety across components. The compiler splits the multitier program into the component-specific code and automatically generates the communication boilerplate. Communication between components can be modeled by declaratively specifying data flows between components using reactive programming. In this paper, we report on the implementation of our design and our experience with embedding our language features into Scala as a host language. We show how a combination of Scalas advanced type level programming and its macro system can be used to enrich the language with new abstractions. We comment on the challenges we encountered and the solutions we developed for our current implementation and outline suggestions for an improved macro system to support the such use cases of embedding of domain-specific abstractions.
We present Choral, the first language for programming choreographies (multiparty protocols) that builds on top of mainstream programming abstractions: in Choral, choreographies are objects. Given a choreography that defines interactions among some roles (Alice, Bob, etc.), an implementation for each role in the choreography is automatically generated by a compiler. These implementations are libraries in pure Java, which developers can modularly compose in their own programs to participate correctly in choreographies.
Recently, Wadler presented a continuation-passing translation from a session-typed functional language, GV, to a process calculus based on classical linear logic, CP. However, this translation is one-way: CP is more expressive than GV. We propose an extension of GV, called HGV, and give translations showing that it is as expressive as CP. The new translations shed light both on the original translation from GV to CP, and on the limitations in expressiveness of GV.
Log in to be able to interact and post comments
comments
Fetching comments
Sign in to be able to follow your search criteria
