-
On the Formalization of Imperative Object-based Calculiin (Co)Inductive Type ...
In this paper, we study the formalization of Abadi and Cardelli's impsigma, a representative object-based calculus with types and side effects, in interactive proof... -
An Open Logical Framework
International audience -
Development and verification of probability logics and logical frameworks
We introduce a Probability Logic with Conditional Operators - LPCP, its syntax, semantics, and a sound and strongly-complete axiomatic system, featuring an infinitary... -
A Logical Framework for Systems Biology
We propose a novel approach for the formal verification of biological systems based on the use of a modal linear logic. We show how such a logic can be used, with... -
Proof-search in Type-theoretic Languages: An Introduction
Article dans revue scientifique avec comité de lecture.
