相关论文: Trocq: Proof Transfer for Free, With or Without Un…
DHOL is an extensional, classical logic that equips the well-known higher-order logic (HOL) with dependent types. This allows for concise encodings of important domains like size-bounded data structures, category theory, or proof theory.…
In this paper, we analyze and compare three of the many algebraic structures that have been used for modeling dependent type theories: categories with families, split type-categories, and representable maps of presheaves. We study these in…
Choreographic programming is a paradigm for writing coordination plans for distributed systems from a global point of view, from which correct-by-construction decentralised implementations can be generated automatically. Theory of…
We present Proof-of-Perception (PoP), a tool-using framework that casts multimodal reasoning as an executable graph with explicit reliability guarantees. Each perception or logic node outputs a conformal set, yielding calibrated, stepwise…
What provides the highest level of assurance for correctness of execution within a programming language? One answer, and our solution in particular, to this problem is to provide a formalization for, if it exists, the denotational semantics…
We develop synthetic notions of oracle computability and Turing reducibility in the Calculus of Inductive Constructions (CIC), the constructive type theory underlying the Coq proof assistant. As usual in synthetic approaches, we employ a…
Automated theorem proving is fundamental to formal methods, and the recent trend is to integrate large language models (LLMs) and proof assistants to form effective proof agents. While existing proof agents show promising performance, they…
This paper presents a case study of formalizing a normalization proof for Leivant's Predicative System F using the Equations package. Leivant's Predicative System F is a stratified version of System F, where type quantification is annotated…
In principle, the design of transition-based dependency parsers makes it possible to experiment with any general-purpose classifier without other changes to the parsing algorithm. In practice, however, it often takes substantial software…
Bibliometrics is useful to analyze the research impact for measuring the research quality. Different bibliographic databases like Scopus, Web of Science, Google Scholar etc. are accessed for evaluating the trend of publications and…
Formal proofs are challenging to write even for experienced experts. Recent progress in Neural Theorem Proving (NTP) shows promise in expediting this process. However, the formal corpora available on the Internet are limited compared to the…
The term UniMath refers both to a formal system for mathematics, as well as a computer-checked library of mathematics formalized in that system. The UniMath system is a core dependent type theory, augmented by the univalence axiom. The…
The connection method has earned good reputation in the area of automated theorem proving, due to its simplicity, efficiency and rational use of memory. This method has been applied recently in automatic provers that reason over ontologies…
In a previous work De Luca and Luna presented formal specifications of idealized formulations of the permission model of Android in the Coq proof assistant. This formal development is about 23 KLOC of Coq code, including proofs. This work…
The use of function contracts to specify the behavior of functions often remains limited to the scope of a single function call. Relational properties link several function calls together within a single specification. They can express more…
Formally verifying system properties is one of the most effective ways of improving system quality, but its high manual effort requirements often render it prohibitively expensive. Tools that automate formal verification, by learning from…
Differentiable logics are a family of quantitative logics originated in the machine learning literature. Because of their origin, differentiable logics often come equipped with analytic properties that guarantee that they are…
Transition-based dependency parsers often need sequences of local shift and reduce operations to produce certain attachments. Correct individual decisions hence require global information about the sentence context and mistakes cause error…
The goal of this lecture is to show how modern theorem provers---in this case, the Coq proof assistant---can be used to mechanize the specification of programming languages and their semantics, and to reason over individual programs and…
Proof assistants are computer softwares that allow us to write mathematical proofs so as to assess their correctness. In November 2021, I started the project of checking the simplicity of the alternating groups within the Lean theorem…