Extensible Object-Theories in HOL-OCL

Channel:
Microsoft Research
Subscribers:
344,000
Published on ● Video Link: https://www.youtube.com/watch?v=rZY9cD1605c


Duration: 59:59
70 views
2

We present a datatype package that enables the shallow embedding technique to object-oriented specification and programming languages. The package incrementally compiles an object-oriented data model to a theory containing object-universes, constructors, and accessors functions, coercions between dynamic and static types, class invariants, and their relations reflecting inheritance. The package is conservative, i.e., all properties are derived entirely from axiomatic definitions. As an application, we use the package for a object-oriented core-language called IMP++, for which correctness of a Hoare-Logic with respect to an operational semantics is proven.



Other Videos By Microsoft Research


2016-09-07Robust Constrained GSC Algorithm for Microphone Array Processing
2016-09-07Robust Speaker Diarization for Meetings: the ICSI system
2016-09-07Evaluating Interactive Gaming as a Language Learning Tool
2016-09-07Resource management of heterogeneous wireless networks
2016-09-07Behind the Code with Jim Gray
2016-09-07Model-based testing with labeled transition systems [1/2]
2016-09-07Interruptions On Software Teams: A Comparison of Paired and Solo Programmers
2016-09-07A Rewriting Logic Sampler
2016-09-07Generalized algebraic data types and all that
2016-09-07Beyond bag-of-features: adding spatial and shape information
2016-09-07Extensible Object-Theories in HOL-OCL
2016-09-07From Software Engineering to Software as Service: Computing Task Dependencies from Work Artifacts
2016-09-07Inferring Faults from Persistent State Interactions
2016-09-07Enhanced MVDR beamforming for Arrays of Directional Microphones
2016-09-07When Separation Logic met Java
2016-09-07Microphone Array for Audience Capture in Lecture Rooms
2016-09-07Learning to Label Images
2016-09-07On the Compressibility of NP Instances and Cryptographic Applications
2016-09-07Search: Use of Relevance Feedback and Estimating Effectiveness of Searches
2016-09-07Tool Support for Proof Engineering
2016-09-07Attack-Resistant Algorithms for Massive Networks


Tags:
microsoft research