ESOP 2010 - PDF Preprint Papers

ESOP 2010 European Symposium on Programming

Teaser Browsing | Click Here

Title Browsing | Click Here

Wall of Fame | Most Viewed ESOP-2010 Paper

click to vote

ESOP
2010
Springer

279views Programming Languages» more ESOP 2010»

A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While

14 years 1 months ago

Download www.cs.ioc.ee

In search for a foundational framework for reasoning about observable behavior of programs that may not terminate, we have previously devised a trace-based big-step semantics for W...

Keiko Nakata and Tarmo Uustalu

claim paper

Read More »

Disclaimer and Copyright Notice

Sciweavers respects the rights of all copyright holders and in this regard, authors are only allowed to share a link to their preprint paper on their own website. Every contribution is associated with a desciptive image. It is the sole responsibility of the authors to ensure that their posted image is not copyright infringing. This service is compliant with IEEE copyright.

Id	Views	Title	Status

1	279	A Hoare Logic for the Coinductive Trace-Based Big-Step Semantics of While	claim
2	219	Precise and Automated Contract-based Reasoning for Verification and Certification of Information Flow Properties of Programs wit	claim
3	217	Automating Security Mediation Placement
4	195	Amortized Resource Analysis with Polynomial Potential - A Static Inference of Polynomial Bounds for Functional Programs	claim
5	189	Verifying a Compiler for Java Threads	claim
6	184	Enforcing Stateful Authorization and Information Flow Policies in Fine	claim
7	178	Parameterized Memory Models and Concurrent Separation Logic	claim
8	177	Faulty Logic: Reasoning about Fault Tolerant Programs	claim
9	176	CFA2: A Context-Free Approach to Control-Flow Analysis	claim
10	174	Amortised Resource Analysis with Separation Logic	claim
11	169	Propositional Interpolation and Abstract Interpretation	claim
12	168	Explicit Stabilisation for Modular Rely-Guarantee Reasoning	claim
13	167	A theory of speculative computation	claim
14	160	A Semantic Framework for Declassification and Endorsement	claim
15	157	Generative Operational Semantics for Relaxed Memory Models	claim
16	157	A Universal Calculus for Stream Processing Languages	claim
17	155	On the Expressive Power of Primitives for Compensation Handling	claim
18	150	Amortized Resource Analysis with Polynomial Potential	claim
19	150	TRX: A Formally Verified Parser Interpreter	claim
20	148	Functional Programming in Sublinear Space	claim
21	148	Separating Shape Graphs	claim
22	144	Deadlock-free Channels and Locks	claim
23	142	Weighted Dynamic Pushdown Networks	claim
24	130	Stateful Contracts for Affine Types	claim
25	128	Logical Concurrency Control From Sequential Proofs	claim
26	126	Testing Polymorphic Properties	claim
27	120	Dynamic Boundaries: Information Hiding by Second Order Framing with First Order Assertions	claim
28	118	Formal Verification of Coalescing Graph-Coloring Register Allocation	claim
29	115	A PolyTime Functional Language from Light Linear Logic	claim
30	114	Fluid Updates: Beyond Strong vs. Weak Updates	claim
31	109	A Grammar-based Approach to Invertible Programs	claim

Sciweavers

Explore & Download

Productivity Tools

Document Tools

Image Tools

Sciweavers