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. Automation support is obtained by translating DHOL to HOL, for which powerful modern automated theorem provers are available. However, a critically missing feature of DHOL is polymorphism. We develop the syntax and semantics of polymorphic DHOL and extend the translation accordingly. We implement the translation in the logic-embedding tool and evaluate it on a range of TPTP formalizations. The logic-embedding tool, together with an off-the-shelf HOL theorem prover easily creates a PDHOL theorem prover for experimenting.

Abstract Both higher-order logic and dependent types are popular features for languages used for the formalization of complex domains. Recently DHOL was introduced as a language that provides the expressivity of dependent types while retaining the general feel of higher-order logic. Since then multiple extensions and theorem provers have been developed, and DHOL was adopted as the first TPTP standard for using dependent types in automated theorem provers. However, the literature lacks a model theoretical semantics for DHOL. The present paper fills in this gap, covering dependent types, rank-1 polymorphism, and functions with preconditions. It introduces both standard models and an appropriate generalization of Henkin-style models and proves soundness and completeness. Considerable care went into keeping the formulation as close to the usual definitions for HOL and elegant enough to serve as a reference point for language extensions and theorem provers for DHOL.

All critical systems must evolve to meet the needs of a growing and diversifying user base. But supporting that evolution is challenging at increasing scale: Maintainers must find a way to ensure that each change does only what is intended, and will not inadvertently change behavior for existing users. This paper presents how we addressed this challenge for the Amazon Web Services (AWS) authorization engine, invoked 1 billion times per second, by using formal verification. Over a period of four years, we built a new authorization engine, one that behaves functionally the same as its predecessor, using the verification-aware programming language Dafny. We can now confidently deploy enhancements and optimizations while maintaining the highest assurance of both correctness and backward compatibility. We deployed the new engine in 2024 without incident and customers immediately enjoyed a threefold performance improvement. The methodology we followed to build this new engine was not an off-the-shelf application of an existing verification tool, and this paper presents several key insights: 1) Rather than prove correct the existing engine, written in Java, we found it more effective to write a new engine in Dafny, a language built for verification from the ground up, and then compile the result to Java. 2) To ensure performance, debuggability, and to gain trust from stakeholders, we needed to generate readable, idiomatic Java code, essentially a transliteration of the source Dafny. 3) To ensure that the specification matches the system's actual behavior, we performed extensive differential and shadow testing throughout the development process, ultimately comparing against 1015production samples prior to deployment. Our approach demonstrates how formal verification can be effectively applied to evolve critical legacy software at scale.

Abstract Higher-order logic HOL offers a very simple syntax and semantics for representing and reasoning about typed data structures. But its type system lacks advanced features where types may depend on terms. Dependent type theory offers such a rich type system, but has rather substantial conceptual differences to HOL, as well as comparatively poor proof automation support. We introduce a dependently-typed extension DHOL of HOL that retains the style and conceptual framework of HOL. Moreover, we build a translation from DHOL to HOL and implement it as a preprocessor to a HOL theorem prover, thereby obtaining a theorem prover for DHOL.

Abstract The interoperability of proof assistants and the integration of their libraries is a highly valued but elusive goal in the field of theorem proving. As a preparatory step, in previous work, we translated the libraries of multiple proof assistants, specifically the ones of Coq, HOL Light, IMPS, Isabelle, Mizar, and PVS into a universal format: OMDoc/MMT. Each translation presented great theoretical, technical, and social challenges, some universal and some system-specific, some solvable and some still open. In this paper, we survey these challenges and compare and evaluate the solutions we chose. We believe similar library translations will be an essential part of any future system interoperability solution, and our experiences will prove valuable to others undertaking such efforts.

M mt is a framework for designing and implementing formal systems in a way that systematically abstracts from theoretical and practical aspects of their type of theoretical and logical foundations. Thus, definitions, theorems, and algorithms can be stated independently of the foundation, and language designers can focus on the essentials of a particular foundation and inherit a large-scale implementation from M mt at low cost. Going beyond the similarly motivated approach of meta-logical frameworks, M mt does not even commit to a particular meta-logic—that makes M mt level results harder to obtain but also more general. We present one such result: a type reconstruction algorithm that realizes the foundation-independent aspects generically relative to a set of rules that supply the foundation-specific knowledge. Maybe surprisingly, we see that the former covers most of the algorithm, including the most difficult details. Thus, we can easily instantiate our algorithm with rule sets for several important language features including, e.g., dependent function types. Moreover, our design is modular such that we obtain a type reconstruction algorithm for any combination of these features.

We give general definitions of logical frameworks and logics. Examples include the logical frameworks LF and Isabelle and the logics represented in them. We apply this to give general definitions for equivalence of logics, translation between logics and combination of logics. We also establish general criteria for the soundness and completeness of these. Our key messages are that the syntax and proof systems of logics are theories; that both semantics and translations are theory morphisms; and that combinations are colimits. Our approach is based on the Mmt language, which lets us combine formalist declarative representations (and thus the associated tool support) with abstract categorical conceptualizations.

When relating formal languages, e.g., in logic or type theory, it is often important to establish representation theorems. These interpret one language in terms of another in a way that preserves semantic properties such as provability or typing. Metalanguages for stating representation theorems can be divided into two groups: First, computational languages are very expressive (usually Turing-complete), but verifying the representation theorems is very difficult (often prohibitively so); second, declarative languages are restricted to certain classes of representation theorems (often based on theory morphisms), for which correctness is decidable. Neither is satisfactory, and this article contributes to the investigation of the trade-off between these two methods. Concretely, we introduce lax theory morphisms, which combine some of the advantages of each: they are substantially more expressive than conventional theory morphisms, but they share many of the invariants that make theory morphisms easy to work with. Specifically, we introduce lax morphisms between theories of a dependently typed logical framework, but our approach and results carry over to most declarative metalanguages. We demonstrate the usefulness of lax theory morphisms by stating and verifying a type erasure translation from typed to untyped first-order logic. The translation is stated as a single lax theory morphism, and the invariants of the framework guarantee its correctness. This is the first time such a complex translation has be verified in a declarative framework.

Mathematical logic and computer science have driven the design of a growing number of logics and related formalisms such as set theories and type theories. In response to this population explosion, logical frameworks have been developed as formal meta-languages in which to represent, structure, relate and reason about logics. Research on logical frameworks has diverged into separate communities, often with conflicting backgrounds and philosophies. In particular, two of the most important logical frameworks are the framework of institutions, from the area of model theory based on category theory, and the Edinburgh Logical Framework LF, from the area of proof theory based on dependent type theory. Even though their ultimate motivations overlap – for example in applications to software verification – they have fundamentally different perspectives on logic. In the current paper, we design a logical framework that integrates the frameworks of institutions and LF in a way that combines their complementary advantages while retaining the elegance of each of them. In particular, our framework takes a balanced approach between model theory and proof theory, and permits the representation of logics in a way that comprises all major ingredients of a logic: syntax, models, satisfaction, judgments and proofs. This provides a theoretical basis for the systematic study of logics in a comprehensive logical framework. Our framework has been applied to obtain a large library of structured and machine-verified encodings of logics and logic translations.

Logical relations are a central concept used to study various higher-order type theories and occur frequently in the proofs of a wide variety of meta-theorems. Besides extending the logical relation principle to more general languages, an important research question has been how to represent and thus verify logical relation arguments in logical frameworks. We formulate a theory of logical relations for Dependent Type Theory (DTT) with β η-equality which guarantees that any valid logical relation satisfies the Basic Lemma. Our definition is syntactic and reflective in the sense that a relation at a type is represented as a DTT type family but also permits expressing certain semantic definitions. We use the Edinburgh Logical Framework (LF) incarnation of DTT and implement our notion of logical relations in the type-checker Twelf. This enables us to formalize and mechanically decide the validity of logical relation arguments. Furthermore, our implementation includes a module system so that logical relations can be built modularly. We validate our approach by formalizing and verifying several syntactic and semantic meta-theorems in Twelf. Moreover, we show how object languages encoded in DTT can inherit a notion of logical relation from the logical framework.

Over recent decades there has been a trend towards formalised mathematics, and a number of sophisticated systems have been developed both to support the formalisation process and to verify the results mechanically. However, each tool is based on a specific foundation of mathematics, and formalisations in different systems are not necessarily compatible. Therefore, the integration of these foundations has received growing interest. We contribute to this goal by using LF as a foundational framework in which the mathematical foundations themselves can be formalised and therefore also the relations between them. We represent three of the most important foundations – Isabelle/HOL, Mizar and ZFC set theory – as well as relations between them. The relations are formalised in such a way that the framework permits the extraction of translation functions, which are guaranteed to be well defined and sound. Our work provides the starting point for a systematic study of formalised foundations in order to compare, relate and integrate them.