Related papers: Type-Based Incorrectness Reasoning
Code language models are increasingly adopted for both understanding and generative tasks. Despite their success, these models frequently produce overconfident incorrect predictions and underconfident correct predictions, undermining their…
Session types capture precise protocol structure in concurrent programming, but do not specify properties of the exchanged values beyond their basic type. Refinement types are a form of dependent types that can address this limitation,…
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…
In sequential functional languages, sized types enable termination checking of programs with complex patterns of recursion in the presence of mixed inductive-coinductive types. In this paper, we adapt sized types and their metatheory to the…
Refinement types enable lightweight verification of functional programs. Algorithms for statically inferring refinement types typically work by reduction to solving systems of constrained Horn clauses extracted from typing derivations. An…
This thesis embarks on a comprehensive exploration of formal computational models that underlie typed programming languages. We focus on programming calculi, both functional (sequential) and concurrent, as they provide a compelling rigorous…
We present a unifying framework for type systems for process calculi. The core of the system provides an accurate correspondence between essentially functional processes and linear logic proofs; fragments of this system correspond to…
Practical checkers based on refinement types use the combination of implicit semantic sub-typing and parametric polymorphism to simplify the specification and automate the verification of sophisticated properties of programs. However, a…
We present a type theory combining both linearity and dependency by stratifying typing rules into a level for logics and a level for programs. The distinction between logics and programs decouples their semantics, allowing the type system…
Software Model Checkers have shown outstanding performance improvements in recent times. Moreover, for specific use cases, formal verification techniques have shown to be highly effective, leading to a number of high-profile success…
Formal deductive systems are very common in computer science. They are used to represent logics, programming languages, and security systems. Moreover, writing programs that manipulate them and that reason about them is important and…
We present an automated framework for solidifying the cohesion between software specifications, their dependently typed models, and implementation at compile time. Model Checking and type checking are currently separate techniques for…
The pattern-match safety problem is to verify that a given functional program will never crash due to non-exhaustive patterns in its function definitions. We present a refinement type system that can be used to solve this problem. The…
Pattern-matching programming is an example of a rule-based programming style developed in functional languages. This programming style is intensively used in dialects of ML but is restricted to algebraic data-types. This restriction limits…
Among the various forms of reasoning studied in the context of artificial intelligence, qualitative reasoning makes it possible to infer new knowledge in the context of imprecise, incomplete information without numerical values. In this…
We propose a method for inferring \emph{parameterized regular types} for logic programs as solutions for systems of constraints over sets of finite ground Herbrand terms (set constraint systems). Such parameterized regular types generalize…
Refinement types are types equipped with predicates that specify preconditions and postconditions of underlying functional languages. We propose a general semantic construction of dependent refinement type systems from underlying type…
In the theory of programming languages, type inference is the process of inferring the type of an expression automatically, often making use of information from the context in which the expression appears. Such mechanisms turn out to be…
This paper introduces an explanation framework designed to enhance the quality of rules in knowledge-based reasoning systems based on dataset-driven insights. The traditional method for rule induction from data typically requires…
Type refinements combine the compositionality of typechecking with the expressivity of program logics, offering a synergistic approach to program verification. In this paper we apply dependent type refinements to SAX, a futures-based…