Related papers: Unifying type systems for mobile processes
We propose a type-based analysis to infer the session protocols of channels in an ML-like concurrent functional language. Combining and extending well-known techniques, we develop a type-checking system that separates the underlying ML type…
Linear Logic refines Intuitionnistic Logic by taking into account the resources used during the proof and program computation. In the past decades, it has been extended to various frameworks. The most famous are indexed linear logics which…
Cycle-accurate software simulation of multicores with complex microarchitectures is often excruciatingly slow. People use simplified core models to gain simulation speed. However, a persistent question is to what extent the results derived…
Path polymorphism is the ability to define functions that can operate uniformly over arbitrary recursively specified data structures. Its essence is captured by patterns of the form $x\,y$ which decompose a compound data structure into its…
This paper synthesizes a series of formal proofs to construct a unified theory on the logical limits of the Symbol Grounding Problem. We distinguish between internal meaning (sense), which formal systems can possess via axioms, and external…
Conceptual modeling is an essential tool in many fields of study, including security specification in information technology systems. As a model, it restricts access to resources and identifies possible threats to the system. We claim that…
Mathematical models are increasingly used in both academia and the pharmaceutical industry to understand how phenotypes emerge from systems of molecular interactions. However, their current construction as monolithic sets of equations…
This dissertation introduces executable refinement types, which refine structural types by semi-decidable predicates, and establishes their metatheory and accompanying implementation techniques. These results are useful for undecidable type…
Gradual dependent types can help with the incremental adoption of dependently typed code by providing a principled semantics for imprecise types and proofs, where some parts have been omitted. Current theories of gradual dependent types,…
We propose the concept of adaptable processes as a way of overcoming the limitations that process calculi have for describing patterns of dynamic process evolution. Such patterns rely on direct ways of controlling the behavior and location…
We present a type checking algorithm for establishing a session-based discipline in the pi calculus of Milner, Parrow and Walker. Our session types are qualified as linear or unrestricted. Linearly typed communication channels are…
This paper explores proof-theoretic aspects of hybrid type-logical grammars , a logic combining Lambek grammars with lambda grammars. We prove some basic properties of the calculus, such as normalisation and the subformula property and also…
We show that time complexity analysis of higher-order functional programs can be effectively reduced to an arguably simpler (although computationally equivalent) verification problem, namely checking first-order inequalities for validity.…
While model checking has often been considered as a practical alternative to building formal proofs, we argue here that the theory of sequent calculus proofs can be used to provide an appealing foundation for model checking. Since the…
A type theory is presented that combines (intuitionistic) linear types with type dependency, thus properly generalising both intuitionistic dependent type theory and full linear logic. A syntax and complete categorical semantics are…
While methods of code abstraction and reuse are widespread and well researched, methods of proof abstraction and reuse are still emerging. We consider the use of dependent types for this purpose, introducing a completely mechanical approach…
The dependently-typed lambda calculus LF is often used as a vehicle for formalizing rule-based descriptions of object systems. Proving properties of object systems encoded in this fashion requires reasoning about formulas over LF typing…
We describe the use of quantum process calculus to describe and analyze quantum communication protocols, following the successful field of formal methods from classical computer science. The key idea is to define two systems, one modelling…
A fundamental task for propositional logic is to compute models of propositional formulas. Programs developed for this task are called satisfiability solvers. We show that transition systems introduced by Nieuwenhuis, Oliveras, and Tinelli…
Harnessing parallelism in seemingly sequential models is a central challenge for modern machine learning. Several approaches have been proposed for evaluating sequential processes in parallel using iterative fixed-point methods, like…