Publications associées à Sémantique des langages de programmation

Orthologic with Axioms

We study the proof theory and algorithms for orthologic, a logical system based on ortholattices, which have shown practical relevance in simplification and normalization of verification conditions. Ortholattices weaken Boolean algebras while having polyno ...

Association for Computing Machinery2024

Dynamic Linkers Are the Narrow Waist of Operating Systems

Adrien Ghosn, Charly Nicolas Lucien Castes

While software applications, programming languages, and hardware have changed, operating systems have not. Widely-used commodity operating systems are still modeled after the ones designed in the seventies. The accumulated burden of backward compatibility ...

Association for Computing Machinery2023

Direct Model-checking of SysML Models

Alessandro Tempia Calvino

Model-checking intends to verify whether a property is satisfied by a model, or not. Model-checking of high-level models, e.g. SysML models, usually first requires a model transformation to a low level formal specification. The present papers proposes a ne ...

SCITEPRESS2021

Verification of Software Network Functions with No Verification Expertise

Arseniy Zaostrovnykh

Software network functions (NFs), such as a network address translator, load balancer, or proxy, promise to bring flexibility and rapid innovation to computer networks and to reduce operational costs. However, continuous updates and flexibility typically c ...

EPFL2020

Simplicitly: Foundations and Applications of Implicit Function Types

Martin Odersky, Heather Christine Klug, Fengyun Liu, Sandro Stucki, Olivier Eric Paul Blanvillain

Understanding a program entails understanding its context; dependencies, configurations and even implementations are all forms of contexts. Modern programming languages and theorem provers offer an array of constructs to define contexts, implicitly. Scala ...

2017

Type Soundness Proofs with Definitional Interpreters

Tiark Rompf, Nada Amin

While type soundness proofs are taught in every graduate PL class, the gap between realistic languages and what is accessible to formal proofs is large. In the case of Scala, it has been shown that its formal model, the Dependent Object Types (DOT) calculu ...

Assoc Computing Machinery2017

Exogenous Coordination of Concurrent Software Components with JavaBIP

Simon Bliudze, Anastasia Mavridou, Radoslaw Szymanek, Alina Zolotukhina

A strong separation of concerns is necessary in order to make the design of domain-specific functional components independent from cross-cutting concerns, such as concurrent access to the shared resources of the execution platform. Native coordination mech ...

Wiley-Blackwell2017

A Formally Verified NAT

George Candea, Solal Vincenzo Pirelli, Aikaterini Argyraki, Arseniy Zaostrovnykh, Luis David Figueiredo Mascarenhas Moreira Pedrosa

We present a Network Address Translator (NAT) written in C and proven to be semantically correct according to RFC 3022, as well as crash-free and memory-safe. There exists a lot of recent work on network verification, but it mostly assumes models of networ ...

Assoc Computing Machinery2017

A Historical Review of Diachrony and Semantic Dimensions of Trace in Neurosciences and Lacanian Psychoanalysis

Pierre Magistretti

Experience leaves a trace in the nervous system through plasticity. However, the exact meaning of the mnesic trace is poorly defined in current literature. This article provides a historical review of the term trace in neuroscience and psychoanalysis liter ...

Frontiers Media2017

Coordination of Dynamic Software Components with JavaBIP

Simon Bliudze, Anastasia Mavridou

JavaBIP allows the coordination of software components by clearly separating the functional and coordination aspects of the system behavior. JavaBIP implements the principles of the BIP component framework rooted in rigorous operational semantics. Recent w ...

Springer International Publishing2017