编程语言
Free monads (and their variants) have become a popular general-purpose tool for representing the semantics of effectful programs in proof assistants. These data structures support the compositional definition of semantics parameterized by…
Teaching programming to novices is best done with tools with simpler user interfaces than professional IDEs that are tailored for experienced programmers. In a distance learning situation it is also important to have a development…
We present a novel approach for teaching logic and the metatheory of logic to students who have some experience with functional programming. We define concepts in logic as a series of functional programs in the language of the proof…
We report on a one-semester compiler construction course based on the idea of implementing a small self-contained compiler for a small model language from scratch, not using other compiler construction frameworks. The course is built around…
Integrated Development Environments (IDEs) provide tool support to automate many source code editing tasks. Traditionally, IDEs use only the spatial context, i.e., the location where the developer is editing, to generate candidate edit…
Model Checking is widely applied in verifying the correctness of complex and concurrent systems against a specification. Pure symbolic approaches while popular, still suffer from the state space explosion problem that makes them impractical…
Inspired by computability logic\cite{Jap03}, we refine recursive function definitions into two kinds: blindly-quantified (BQ) ones and parallel universally quantified (PUQ) ones. BQ definitions corresponds to the traditional ones where…
This volume contains the papers, accepted after post-reviewing, based on presentations submitted to TFPIE 2021 and TFPIE 2022 that took place online, in collaboration with LambdaDays 2021/22 in Krak\'ow, Poland. TFPIE stands for Trends in…
CoqQ is a framework for reasoning about quantum programs in the Coq proof assistant. Its main components are: a deeply embedded quantum programming language, in which classic quantum algorithms are easily expressed, and an expressive…
Type systems usually characterize the shape of values but not their free variables. However, many desirable safety properties could be guaranteed if one knew the free variables captured by values. We describe CCsubBox, a calculus where such…
A linear parameter must be consumed exactly once in the body of its function. When declaring resources such as file handles and manually managed memory as linear arguments, a linear type system can verify that these resources are used…
We develop the first theory of control-flow graphs from first principles, and use it to create an algorithm for automatically synthesizing many variants of control-flow graph generators from a language's operational semantics. Our approach…
Type-and-effect systems are a widely-used approach to program verification, verifying the result of a computation using types, and the behavior using effects. This paper extends an effect system for verifying temporal, value-dependent…
FreezeML is a new approach to first-class polymorphic type inference that employs term annotations to control when and how polymorphic types are instantiated and generalised. It conservatively extends Hindley-Milner type inference and was…
This article describes the features of a compiler for a superset language of the well-known PL/0 created by Niklaus Wirth. The main feature is that it implements the build phases in such a way that the information passed between each one is…
Choreographies are formal descriptions of distributed systems, which focus on the way in which participants communicate. While they are useful for analysing protocols, in practice systems are written directly by specifying each…
Refinement type checkers are a powerful way to reason about functional programs. For example, one can prove properties of a slow, specification implementation, porting the proofs to an optimized implementation that behaves the same. Without…
Web applications are structured as multi-tier stacks of components. Each component may be written in a different language and interoperate using a variety of protocols. Such interoperation increases developer effort, can introduce security…
Static analyses based on typestates are important in certifying correctness of code contracts. Such analyses rely on Deterministic Finite Automata (DFAs) to specify properties of an object. We target the analysis of contracts in low-latency…
This talk presents Gopcaml-mode, the first structural editing plugin for OCaml. We will give a tour of the main plugin features, discussing the plugin's internal design and its integration with existing OCaml and GNU Emacs toolchains.