GitPlanet

Cheap and reliable Node.js hosting starts at $3/month, and $1/month static HTML hosting

Created with love in Canada, visit hostnodejs.com today

Feel like to post an Ad? Learn Details
All Projects → matthesjh → coq-tal

matthesjh / coq-tal

Licence: MIT license
Formalization of Typed Assembly Language (TAL) in Coq

Programming Languages

Coq
218 projects
shell
77523 projects

Labels

coqtype-systemtal

Projects that are alternatives of or similar to coq-tal

Fscq
FSCQ is a certified file system written and proven in Coq
Stars: ✭ 208 (+1286.67%)
Mutual labels:  coq
Truth
A Domain Representation Language
Stars: ✭ 23 (+53.33%)
Mutual labels:  type-system
coq-ecosystem
No description or website provided.
Stars: ✭ 39 (+160%)
Mutual labels:  coq
Vellvm
The Vellvm (Verified LLVM) coq development.
Stars: ✭ 243 (+1520%)
Mutual labels:  coq
WasmCert-Coq
A mechanisation of Wasm in Coq
Stars: ✭ 68 (+353.33%)
Mutual labels:  coq
coq-100-theorems
Statements of famous theorems proven in Coq [maintainer=@jmadiot]
Stars: ✭ 41 (+173.33%)
Mutual labels:  coq
Metacoq
Metaprogramming in Coq
Stars: ✭ 192 (+1180%)
Mutual labels:  coq
koika
A core language for rule-based hardware design 🦑
Stars: ✭ 103 (+586.67%)
Mutual labels:  coq
iris-simp-lang
We define a simple programming language, simp_lang, then instantiate Iris to verify simple simp_lang programs with concurrent separation logic.
Stars: ✭ 40 (+166.67%)
Mutual labels:  coq
CoqCheatSheet
Reference sheet for the Coq language.
Stars: ✭ 15 (+0%)
Mutual labels:  coq
f-omega-mu
Fωμ type checker and compiler
Stars: ✭ 46 (+206.67%)
Mutual labels:  type-system
goose
Goose converts a small subset of Go to Coq
Stars: ✭ 73 (+386.67%)
Mutual labels:  coq
coq-elpi
Coq plugin embedding elpi
Stars: ✭ 92 (+513.33%)
Mutual labels:  coq
Foundations
Voevodsky's original development of the univalent foundations of mathematics in Coq
Stars: ✭ 210 (+1300%)
Mutual labels:  coq
stablesort
Stable sort algorithms and their stability proofs in Coq
Stars: ✭ 19 (+26.67%)
Mutual labels:  coq
Coqgym
A Learning Environment for Theorem Proving with the Coq proof assistant
Stars: ✭ 201 (+1240%)
Mutual labels:  coq
coq-to-ocaml-to-js
Proof of concept to generate safe and fast JavaScript
Stars: ✭ 25 (+66.67%)
Mutual labels:  coq
coqeal
The Coq Effective Algebra Library [maintainers=@CohenCyril,@proux01]
Stars: ✭ 62 (+313.33%)
Mutual labels:  coq
coqffi
Coq to OCaml FFI made easy [maintainer=@lthms]
Stars: ✭ 27 (+80%)
Mutual labels:  coq
toychain
A minimalistic blockchain consensus implemented and verified in Coq
Stars: ✭ 103 (+586.67%)
Mutual labels:  coq
View All Similar Projects ➔

Formalization of Typed Assembly Language (TAL) in Coq

Build project Coq

This repository contains an implementation of Typed Assembly Language, more specifically the simplified version TAL-0, in Coq.

The implementation was developed as part of a master's seminar. It is based on the chapter Typed Assembly Language from the book Advanced Topics in Types and Programming Languages and an already existing (but different) implementation by Ankit Kumar.

Usage

Please make sure that you have installed the Coq Proof Assistant on your operating system. The latest version of Coq can be found here.

Note: The files have been fully tested with Coq versions 8.7.2 to 8.16.0.

In order to compile the Coq files provided by this repository, the _CoqProject file can be used.

coq_makefile -f _CoqProject -o Makefile

This generates a Makefile that can be executed with make. The generated Makefile resolves dependencies and calls the Coq compiler coqc. Subsequently, the files can be opened and imported.

Documentation

The documentation for the Coq files provided by this repository can be found here.

Note that the project description data, including the texts, logos, images, and/or trademarks, for each open source project belongs to its rightful owner. If you wish to add or remove any projects, please contact us at [email protected].