Related papers: Controlling unfolding in type theory
The recently introduced dependent typed higher-order logic (DHOL) offers an interesting compromise between expressiveness and automation support. It sacrifices the decidability of its type system in order to significantly extend its…
This paper describes a procedure that system developers can follow to translate typical mathematical representations of linearized control systems into logic theories. These theories are then used to verify system requirements and find…
The expressiveness of dependent type theory can be extended by identifying types modulo some additional computation rules. But, for preserving the decidability of type-checking or the logical consistency of the system, one must make sure…
Automated theorem provers and formal proof assistants are general reasoning systems that are in theory capable of proving arbitrarily hard theorems, thus solving arbitrary problems reducible to mathematics and logical reasoning. In…
Dependently-typed proof assistants furnish expressive foundations for mechanised mathematics and verified software. However, automation for these systems has been either modest in scope or complex in implementation. We aim to improve the…
We provide a formulation of the univalence axiom in a universe category model of dependent type theory that is convenient to verify in homotopy-theoretic settings. We further develop a strengthening of the univalence axiom, called pointed…
In dependent type theory, being able to refer to a type universe as a term itself increases its expressive power, but requires mechanisms in place to prevent Girard's paradox from introducing logical inconsistency in the presence of…
There is growing acknowledgement within the software engineering community that a theory of software development is needed to integrate the myriad methodologies that are currently popular, some of which are based on opposing perspectives.…
This study provides some results about two-level type-theoretic notions in a way that the proofs are fully formalizable in a proof assistant implementing two-level type theory such as Agda. The difference from prior works is that these…
Categories with families (CwFs) have been used to define the semantics of type theory in type theory. In the setting of Homotopy Type Theory (HoTT), one of the limitations of the traditional notion of CwFs is the requirement to set-truncate…
We develop a theory of decidable inductive invariants for an infinite-state variant of the Applied pi-calculus, with applications to automatic verification of stateful cryptographic protocols with unbounded sessions/nonces. Since the…
Conventional sliding mode controllers are based on the assumption of switching control but a well-known drawback of this approach is the chattering phenomenon. To overcome the undesirable chattering effects, the discontinuity in the control…
The Abella interactive theorem prover has proven to be an effective vehicle for reasoning about relational specifications. However, the system has a limitation that arises from the fact that it is based on a simply typed logic:…
Optimization-based solvers play a central role in a wide range of signal processing and communication tasks. However, their applicability in latency-sensitive systems is limited by the sequential nature of iterative methods and the high…
While language embeddings have been shown to have stereotyping biases, how these biases affect downstream question answering (QA) models remains unexplored. We present UNQOVER, a general framework to probe and quantify biases through…
In many analyses in high energy physics, attempts are made to remove the effects of detector smearing in data by techniques referred to as "unfolding" histograms, thus obtaining estimates of the true values of histogram bin contents. Such…
A hierarchy of type universes is a rudimentary ingredient in the type theories of many proof assistants to prevent the logical inconsistency resulting from combining dependent functions and the type-in-type rule. In this work, we argue that…
This paper develops a process-based account of scientific explanation that reconceives grounding in terms of stabilisation. Grounding theories capture hierarchical dependence but lack criteria for when explanations remain adequate under…
Polymorphic variants are a useful feature of the OCaml language whose current definition and implementation rely on kinding constraints to simulate a subtyping relation via unification. This yields an awkward formalization and results in a…
In their usual form, representation independence metatheorems provide an external guarantee that two implementations of an abstract interface are interchangeable when they are related by an operation-preserving correspondence. If our…