-
Binding Logic: proofs and models
Authors:
Gilles Dowek,
Thérèse Hardin,
Claude Kirchner
Abstract:
We define an extension of predicate logic, called Binding Logic, where variables can be bound in terms and in propositions. We introduce a notion of model for this logic and prove a soundness and completeness theorem for it. This theorem is obtained by encoding this logic back into predicate logic and using the classical soundness and completeness theorem there.
We define an extension of predicate logic, called Binding Logic, where variables can be bound in terms and in propositions. We introduce a notion of model for this logic and prove a soundness and completeness theorem for it. This theorem is obtained by encoding this logic back into predicate logic and using the classical soundness and completeness theorem there.
△ Less
Submitted 25 May, 2023;
originally announced May 2023.
-
Quantifying the Structure of Disordered Materials
Authors:
Thomas J. Hardin,
Michael Chandross,
Rahul Meena,
Spencer Fajardo,
Dimitris Giovanis,
Ioannis G. Kevrekidis,
Michael Falk,
Michael Shields
Abstract:
Durable interest in develo** a framework for the detailed structure of glassy materials has produced numerous structural descriptors that trade off between general applicability and interpretability. However, none approach the combination of simplicity and wide-ranging predictive power of the lattice-grain-defect framework for crystalline materials. Working from the hypothesis that the local ato…
▽ More
Durable interest in develo** a framework for the detailed structure of glassy materials has produced numerous structural descriptors that trade off between general applicability and interpretability. However, none approach the combination of simplicity and wide-ranging predictive power of the lattice-grain-defect framework for crystalline materials. Working from the hypothesis that the local atomic environments of a glassy material are constrained by enthalpy minimization to a low-dimensional manifold in atomic coordinate space, we develop a novel generalized distance function, the Gaussian Integral Inner Product (GIIP) distance, in connection with agglomerative clustering and diffusion maps, to parameterize that manifold. Applying this approach to a two-dimensional model crystal and a three-dimensional binary model metallic glass results in parameters interpretable as coordination number, composition, volumetric strain, and local symmetry. In particular, we show that a more slowly quenched glass has a higher degree of local tetrahedral symmetry at the expense of cyclic symmetry. While these descriptors require post-hoc interpretation, they minimize bias rooted in crystalline materials science and illuminate a range of structural trends that might otherwise be missed.
△ Less
Submitted 14 November, 2022;
originally announced November 2022.
-
Hybridizing matter-wave and classical accelerometers
Authors:
Jean Lautier,
Laurent Volodimer,
Thomas Hardin,
Sebastien Merlet,
Michel Lours,
Franck Pereira Dos Santos,
Arnaud Landragin
Abstract:
We demonstrate a hybrid accelerometer that benefits from the advantages of both conventional and atomic sensors in terms of bandwidth (DC to 430 Hz) and long term stability. First, the use of a real time correction of the atom interferometer phase by the signal from the classical accelerometer enables to run it at best performances without any isolation platform. Second, a servo-lock of the DC com…
▽ More
We demonstrate a hybrid accelerometer that benefits from the advantages of both conventional and atomic sensors in terms of bandwidth (DC to 430 Hz) and long term stability. First, the use of a real time correction of the atom interferometer phase by the signal from the classical accelerometer enables to run it at best performances without any isolation platform. Second, a servo-lock of the DC component of the conventional sensor output signal by the atomic one realizes a hybrid sensor. This method paves the way for applications in geophysics and in inertial navigation as it overcomes the main limitation of atomic accelerometers, namely the dead times between consecutive measurements.
△ Less
Submitted 6 October, 2014; v1 submitted 30 September, 2014;
originally announced October 2014.
-
Experience in using a typed functional language for the development of a security application
Authors:
Damien Doligez,
Christèle Faure,
Thérèse Hardin,
Manuel Maarek
Abstract:
In this paper we present our experience in develo** a security application using a typed functional language. We describe how the formal grounding of its semantic and compiler have allowed for a trustworthy development and have facilitated the fulfillment of the security specification.
In this paper we present our experience in develo** a security application using a typed functional language. We describe how the formal grounding of its semantic and compiler have allowed for a trustworthy development and have facilitated the fulfillment of the security specification.
△ Less
Submitted 26 April, 2014;
originally announced April 2014.
-
Yet Another Deep Embedding of B:Extending de Bruijn Notations
Authors:
Eric Jaeger,
Thérèse Hardin
Abstract:
We present Bicoq3, a deep embedding of the B system in Coq, focusing on the technical aspects of the development. The main subjects discussed are related to the representation of sets and maps, the use of induction principles, and the introduction of a new de Bruijn notation providing solutions to various problems related to the mechanisation of languages and logics.
We present Bicoq3, a deep embedding of the B system in Coq, focusing on the technical aspects of the development. The main subjects discussed are related to the representation of sets and maps, the use of induction principles, and the introduction of a new de Bruijn notation providing solutions to various problems related to the mechanisation of languages and logics.
△ Less
Submitted 23 February, 2009;
originally announced February 2009.
-
A Few Remarks About Formal Development of Secure Systems
Authors:
Eric Jaeger,
Thérèse Hardin
Abstract:
Formal methods provide remarkable tools allowing for high levels of confidence in the correctness of developments. Their use is therefore encouraged, when not required, for the development of systems in which safety or security is mandatory. But effectively specifying a secure system or deriving a secure implementation can be tricky. We propose a review of some classical `gotchas' and other poss…
▽ More
Formal methods provide remarkable tools allowing for high levels of confidence in the correctness of developments. Their use is therefore encouraged, when not required, for the development of systems in which safety or security is mandatory. But effectively specifying a secure system or deriving a secure implementation can be tricky. We propose a review of some classical `gotchas' and other possible sources of concerns with the objective to improve the confidence in formal developments, or at least to better assess the actual confidence level.
△ Less
Submitted 23 February, 2009;
originally announced February 2009.
-
On the implementation of construction functions for non-free concrete data types
Authors:
Frédéric Blanqui,
Thérèse Hardin,
Pierre Weis
Abstract:
Many algorithms use concrete data types with some additional invariants. The set of values satisfying the invariants is often a set of representatives for the equivalence classes of some equational theory. For instance, a sorted list is a particular representative wrt commutativity. Theories like associativity, neutral element, idempotence, etc. are also very common. Now, when one wants to combi…
▽ More
Many algorithms use concrete data types with some additional invariants. The set of values satisfying the invariants is often a set of representatives for the equivalence classes of some equational theory. For instance, a sorted list is a particular representative wrt commutativity. Theories like associativity, neutral element, idempotence, etc. are also very common. Now, when one wants to combine various invariants, it may be difficult to find the suitable representatives and to efficiently implement the invariants. The preservation of invariants throughout the whole program is even more difficult and error prone. Classically, the programmer solves this problem using a combination of two techniques: the definition of appropriate construction functions for the representatives and the consistent usage of these functions ensured via compiler verifications. The common way of ensuring consistency is to use an abstract data type for the representatives; unfortunately, pattern matching on representatives is lost. A more appealing alternative is to define a concrete data type with private constructors so that both compiler verification and pattern matching on representatives are granted. In this paper, we detail the notion of private data type and study the existence of construction functions. We also describe a prototype, called Moca, that addresses the entire problem of...
△ Less
Submitted 5 January, 2007;
originally announced January 2007.
