All Media Types
Foundations of probabilistic programming
Barthe G., Katoen J., Silva A., Cambridge University Press, Cambridge, UK, 2021. 582 pp. Type: Book (978-1-108488-51-8)
This book covers various programming languages for probabilistic programming. The languages are described using syntax, semantics, and examples. It also looks at the theories related to the semantics of probability constructs and discusses the rea...
Oct 18 2021
Foundations of security analysis and design V: FOSAD 2007/2008/2009 tutorial lectures (LNCS 5705)
Aldini A., Barthe G., Gorrieri R. Springer-Verlag, New York, NY, 2009. Type: Divisible Book
This is a compilation of selected tutorial papers from the 2007 to 2009 Foundations of Security Analysis and Design (FOSAD) schools. In the first paper, Escobar, Meadows, and Meseguer describe the Maude-NRL protocol analyzer (Maude-NPA), a model-c...
Mar 10 2010
Certificate translation for optimizing compilers
Barthe G., Grégoire B., Kunz C., Rezk T. ACM Transactions on Programming Languages and Systems 31(5): 1-45, 2009. Type: Article
Compiler verification is an important special case of program verification. It deals with correctness proofs of a program (compiler) that translate input programs into output programs. Barthe et al. tackle an interesting amalgam of the generic and...
Dec 4 2009
Formally verifying information flow type systems for concurrent and thread systems
Barthe G., Nieto L. Formal methods in security engineering (Proceedings of the 2004 ACM Conference on Formal Methods in Security Engineering, Washington DC, USA, Oct 29, 2004) 13-22, 2004. Type: Proceedings
This paper is in the area of theory related to concurrency and threading. It is about reasoning noninterference properties in a concurrent programming language with information flow type systems. The work uses the proof assistant Isabelle/HOL to c...
Jan 12 2005
Reproduction in whole or in part without permission is prohibited. Copyright © 2000-2021 ThinkLoud, Inc.