Related papers: Formalizing the Curry-Howard Correspondence
This work presents a formalization of the theorem of existence of most general unifiers in first-order signatures in the higher-order proof assistant PVS. The distinguishing feature of this formalization is that it remains close to the…
In this article we show that hybrid type-logical grammars are a fragment of first-order linear logic. This embedding result has several important consequences: it not only provides a simple new proof theory for the calculus, thereby…
This paper describes the design and implementation of mechanisms for light-weight inclusion of formal mathematics in informal mathematical writings, particularly in a Web-based setting. This is conceptually done in three stages: (i) by…
The geometric formulation of the Hamilton-Jacobi theory enables us to generalize it to systems of higher-order ordinary differential equations. In this work we introduce the unified Lagrangian-Hamiltonian formalism for the geometric…
In proof theory the notion of canonical proof is rather basic, and it is usually taken for granted that a canonical proof of a sentence must be unique up to certain minor syntactical details (such as, e.g., change of bound variables). When…
While much of the current study on quantum computation employs low-level formalisms such as quantum circuits, several high-level languages/calculi have been recently proposed aiming at structured quantum programming. The current work…
Process theories provide a powerful framework for describing compositional structures across diverse fields, from quantum mechanics to computational linguistics. Traditionally, they have been formalized using symmetric monoidal categories…
This is the full version of a paper submitted to the Computability in Europe (CiE 2023) conference, with all proofs omitted there. In 2012 P. D. Azar and S. Micali introduced a new model of interactive proofs, called "Rational Interactive…
Based on an analysis of the inference rules used, we provide a characterization of the situations in which classical provability entails intuitionistic provability. We then examine the relationship of these derivability notions to uniform…
We present a conceptual framework for extending homomorphic encryption beyond arithmetic or Boolean operations into the domain of intuitionistic logic proofs and, by the Curry-Howard correspondence, into the domain of typed functional…
Since the early twentieth century, it has been understood that mathematical definitions and proofs can be represented in formal systems systems with precise grammars and rules of use. Building on such foundations, computational proof…
In this work, a classical-quantum correspondence for two-level pseudo-Hermitian systems is proposed and analyzed. We show that the presence of a complex external field can be described by a pseudo-Hermitian Hamiltonian if there is a…
For unitary groups associated to a ramified quadratic extension of a $p$-adic field, we define various regular formal moduli spaces of $p$-divisible groups with parahoric levels, characterize exceptional special divisors on them, and…
In reductive proof search, proofs are naturally generalized by solutions, comprising all possibly infinite structures generated by locally correct, bottom-up application of inference rules. We propose an extension of the Curry-Howard…
We develop an extension of institution theory that accommodates implicitly the partiality of the signature morphisms and its syntactic and semantic effects. This is driven primarily by applications to conceptual blending, but other…
Autoformalization, the process of transforming informal mathematical propositions into verifiable formal representations, is a foundational task in automated theorem proving, offering a new perspective on the use of mathematics in both…
We consider several formalizations in the language of second-order arithmetic of "The formula $\phi$ is a theorem of $\omega$-logic", including some which have been studied in the literature and a new variant defined via a least fixed…
This paper contains a discussion of a library of formalized mathematics for the proof assistant Coq which the author worked on in 2011-13.
Formalised libraries of combinatorial mathematics have rapidly expanded over the last five years, but few use one of the most important tools: probability. How can often intuitive probabilistic arguments on the existence of combinatorial…
These notes are an elaboration on: (i) a short course that I gave at the IPhT-Saclay in May-June 2012; (ii) a previous letter on reversibility in quantum mechanics. They present an introductory, but hopefully coherent, view of the main…