Search results: Found 3

Listing 1 - 3 of 3
Sort by
A Machine-Checked, Type-Safe Model of Java Concurrency : Language, Virtual Machine, Memory Model, and Verified Compiler

Author:
ISBN: 9783866448858 Year: Pages: XXI, 412 p. DOI: 10.5445/KSP/1000028867 Language: ENGLISH
Publisher: KIT Scientific Publishing
Subject: Computer Science
Added to DOAB on : 2019-07-30 20:01:59
License:

Loading...
Export citation

Choose an application

Abstract

The Java programming language provides safety and security guarantees such as type safety and its security architecture. They distinguish it from other mainstream programming languages like C and C++. In this work, we develop a machine-checked model of concurrent Java and the Java memory model and investigate the impact of concurrency on these guarantees. From the formal model, we automatically obtain an executable verified compiler to bytecode and a validated virtual machine.

From Formal Semantics to Verified Slicing : A Modular Framework with Applications in Language Based Security

Author:
ISBN: 9783866445949 Year: Pages: XIX, 203 p. DOI: 10.5445/KSP/1000020678 Language: ENGLISH
Publisher: KIT Scientific Publishing
Subject: Computer Science
Added to DOAB on : 2019-07-30 20:02:00
License:

Loading...
Export citation

Choose an application

Abstract

This book presents a modular framework for slicing in the proof assistant Isabelle/HOL which is based on abstract control flow graphs. Building on such abstract structures renders the correctness results language-independent. To prove that they hold for a specific language, it remains to instantiate the framework with this language, which requires a formal semantics of this language in Isabelle/HOL. We show that formal semantics even for sophisticated high-level languages are realizable.

Sémantique formelle: Volume 1

Author:
Book Series: Textbooks in Language Sciences ISBN: 9783961100170 9781977891549 Year: Pages: 498 DOI: 10.5281/zenodo.1000504 Language: French
Publisher: Language Science Press
Subject: Linguistics
Added to DOAB on : 2018-01-13 11:02:32
License:

Loading...
Export citation

Choose an application

Abstract

"For nearly half a century formal semantics has been a prominent area in linguistic theory, developed in a fruitful collaboration among linguists, logicians and philosophers. Formal semantics is sometimes regarded with reluctance (even dreaded) due to its mathematical precision and the apparent complexity of its symbolism. This textbook —the first one of this scope in French— provides a relaxed self-contained introduction to the domain, allowing the reader autonomous progressive study from the basic central concepts to significant innovations that have shaped the domain since Montague’s seminal work. Through its chapters, the book provides acquaintance with elements of scientific methodology generally used in formal semantics. The six chapters, completed with solved exercises, gradually move from basic notions in logic and model-theoretic semantics, to quantification, temporal and modal logic, intensionality, and typed λ-calculus, culminating in compositional semantic analysis at the syntax-semantics interface. This introduction will be supplemented with a second volume that would focus on applications and advances in the field which extend the scope of the formalism.
The book is intended for linguistics undergraduate and postgraduate students and researchers wishing to improve their skills in formal semantics, as well as for students and researchers of other domains, such as philosophy, logic, or computational science."

Listing 1 - 3 of 3
Sort by
Narrow your search

Publisher

KIT Scientific Publishing (2)

Language Science Press (1)


License

CC by-nc-nd (2)

CC by (1)


Language

english (2)

french (1)


Year
From To Submit

2017 (1)

2012 (1)

2011 (1)