coq-club AT inria.fr

Subject: The Coq mailing list

List archive

[Coq-Club] Instruction Set Semantics

From: Gregory Malecha <gmalecha AT gmail.com>
To: Coq Club <coq-club AT inria.fr>
Subject: [Coq-Club] Instruction Set Semantics
Date: Fri, 1 Jun 2018 13:12:41 -0400
Authentication-results: mail2-smtp-roc.national.inria.fr; spf=None smtp.pra=gmalecha AT gmail.com; spf=Pass smtp.mailfrom=gmalecha AT gmail.com; spf=None smtp.helo=postmaster AT mail-lf0-f52.google.com
Ironport-phdr: 9a23:mL65bRBDpqzKz0WFkpDgUyQJP3N1i/DPJgcQr6AfoPdwSPT6osbcNUDSrc9gkEXOFd2Cra4c1qyO6+jJYi8p2d65qncMcZhBBVcuqP49uEgeOvODElDxN/XwbiY3T4xoXV5h+GynYwAOQJ6tL1LdrWev4jEMBx7xKRR6JvjvGo7Vks+7y/2+94fcbglUhDexe69+IAmrpgjNq8cahpdvJLwswRXTuHtIfOpWxWJsJV2Nmhv3+9m98p1+/SlOovwt78FPX7n0cKQ+VrxYES8pM3sp683xtBnMVhWA630BWWgLiBVIAgzF7BbnXpfttybxq+Rw1DWGMcDwULs5Qiqp4bt1RxD0iScHLz85/3/Risxsl6JQvRatqwViz4LIfI2ZMfxzcaTAc9MHXmpBRtheWDBdAo2yaIsPCvAOPeder4Lgo1cDoh+zCQyqCejyyDFHm2X20LU13OohHw/I3xEuEcwSv3nPttr5KL0fXPqpwKXUzzjOae5d1zfn6IjPdxAsufCCXahufsrezkkvDQPEhUiXp4P/OzOayPgCs2iB4OF9Uu+vhGsnpBt1ojex2sgsipPGi5kaylDB7yp5wYI1KcekR058ZN6pCZ1dvDyUOYtxR8MtWWBouCAix70JuJ67YCgKyIk8yBLFavyHdI6F6Q/gWuaJOTp0mm5pdbalixux8UWs0PPwWtS03VpQridJjN/BvW0X2RPJ8MiIUP5981+h2TmR0wDT7flJIUUumqraL54t27owlpQPvUjaEC/7mFv6gLWZdkUj/eio5ODnbav8qpCAMI90jxnyMqUomsOhHeQ1KhYCU3Sf9Oim17Du/Vf1TKtXgvA2iKXUsI7WKdwepqGjAg9V1ogj6wy4DzejyNkYknwHI0hBeB2Zk4fpO0vBLev3Dfe6mVuskTNry+raMb3mB5XBNmLDn6v5fbZh905czxI+wsxY55JNE70OPPbzWlLqu9HDFR84Mwm0w/79B9ln14MeX3iPAq6DP6/Iv1+I/LFnH+7ZT4gM8B35NvJts/XplDoynUIXVaivx5oeLn6iSKdIOUKcNFX2j9gGC3ZCmwM6QefqgRXWXjtaY3u5X6sU6TQyCYbgBoDGENP+yIed1Tu2S8UFLltNDUqBRDK1LtzVCcdJUzqbJ4paqhJBULGgT4E70hT37V31zrNmKqzf/ShK7Mu/hugw3PXakFQJzRIxF96UijjfQGR9n2dOTDgzjvgm/B5Nj2yb2K09uMR2UNxe4/QTD1U/PJ/Yiuh0U5X8B1iHcdCOR1KrBN6hBGNpQw==

Hello --

I am wondering if anyone knows of a formalization of the ARMv8 (or other instruction set) in Coq that is open source. I'm looking for as complete of an instruction set as possible since I am working with low-level systems programs.

Thanks so much.

- gregory malecha
gmalecha.github.io

[Coq-Club] Instruction Set Semantics, Gregory Malecha, 06/01/2018
- Re: [Coq-Club] Instruction Set Semantics, Clément Pit-Claudel, 06/01/2018
- Re: [Coq-Club] Instruction Set Semantics, Frédéric Blanqui, 06/04/2018
- Re: [Coq-Club] Instruction Set Semantics, Peter Sewell, 06/05/2018