2 citations
5 papers
A Formally Specified Type System and Operational Semantics for Higher-Order Procedural Variables
Tristan Crolard, Emmanuel Polonowski
We formally specified the type system and operational semantics of LOOPw with Ott and Isabelle/HOL proof assistant. Moreover, both the type system and the semantics of LOOPw have b…
Deriving SN from PSN: a general proof technique
Emmanuel Polonowski
In the framework of explicit substitutions there is two termination properties: preservation of strong normalization (PSN), and strong normalization (SN). Since there are not easil…
New Choice for Small Universal Devices: Symport/Antiport P Systems
Sergey Verlan, Yurii Rogozhin
Symport/antiport P systems provide a very simple machinery inspired by corresponding operations in the living cell. It turns out that systems of small descriptional complexity are…
How to Guarantee Secrecy for Cryptographic Protocols
Danièle Beauquier, Frédéric Gauche
In this paper we propose a general definition of secrecy for cryptographic protocols in the Dolev-Yao model. We give a sufficient condition ensuring secrecy for protocols where rul…
On the additive theory of prime numbers II
Patrick Cegielski, Denis Richard, Maxim Vsemirnov
The undecidability of the additive theory of primes (with identity) as well as the theory Th(N,+, n -> p\_n), where p\_n denotes the (n+1)-th prime, are open questions. As a possib…