A language-independent proof system for full program equivalence
type: Item
instance of: scholarly article
title: A language-independent proof system for full program equivalence
zbMATH Open document ID: 1355.68051
author: Ştefan Ciobâcă
author: Dorel Lucanu
author: Vlad Rusu
author: Grigore Roşu
published in: Formal Aspects of Computing
publication date: 2017-02-14T00:00:00Z
full work available at URL: icfem-postproceedings-final-version.pdf
Mathematics Subject Classification ID: 68N30
Mathematics Subject Classification ID: 03B70
Mathematics Subject Classification ID: 08A70
zbMATH DE Number: 6684423
zbMATH Keywords: matching logic
zbMATH Keywords: programming language semantics
zbMATH Keywords: program equivalence
zbMATH Keywords: full equivalence
zbMATH Keywords: programming language aggregation
describes a project that uses: Coq
describes a project that uses: SymDiff
describes a project that uses: KJS
describes a project that uses: K-Java
MaRDI profile type: Publication
OpenAlex ID: W2315369658
cites work: State-dependent representation independence
cites work: Computer Aided Verification
cites work: Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
cites work: Simple relational correctness proofs for static analyses and program transformations
cites work: Biorthogonality, step-indexing and compiler correctness
cites work: K-Java: a complete semantics of Java
cites work: A Theoretical Foundation for Programming Languages Aggregation
cites work: All-Path Reachability Logic
cites work: An Institutional Foundation for the $$\mathbb {K}$$K Semantic Framework
cites work: Regression Verification for Multi-threaded Programs
cites work: Q4812966
cites work: Inference rules for proving the equivalence of recursive procedures
cites work: Inference Rules for Proving the Equivalence of Recursive Procedures
cites work: Don't Try to Solve These Problems
cites work: A kripke logical relation between ML and assembly
cites work: The marriage of bisimulations and Kripke logical relations
cites work: Q4375636
cites work: An axiomatic basis for computer programming
cites work: Towards Modularly Comparing Programs Using Automated Theorem Provers
cites work: Program equivalence by circular reasoning
cites work: A generic framework for symbolic execution: a coinductive approach
cites work: Q3992568
cites work: Automated Reasoning
cites work: Q4813228
cites work: From Hoare Logic to Matching Logic Reachability
cites work: Towards a Unified Theory of Operational and Axiomatic Semantics
cites work: One-Path Reachability Logic
cites work: Matching Logic: An Alternative to Hoare/Floyd Logic
cites work: Equality of streams is a Π0 over 2-complete problem
cites work: Matching Logic - Extended Abstract (Invited Talk)
cites work: Introduction to Bisimulation and Coinduction
cites work: Logical Bisimulations and Functional Languages
cites work: A rewriting logic approach to operational semantics
DOI: 10.1007/S00165-016-0361-7
description: scientific article; zbMATH DE number 6684423