Skip to content

Shallow_Micro_Rust

Directory actions

More options

Directory actions

More options

Latest commit

 

History

History

Shallow_Micro_Rust

Folders and files

NameName
Last commit message
Last commit date

parent directory

..
document
document
 
 
Basic_Case_Expression.thy
Basic_Case_Expression.thy
 
 
Bool_Type.thy
Bool_Type.thy
 
 
Bool_Type_Lemmas.thy
Bool_Type_Lemmas.thy
 
 
Core_Expression.thy
Core_Expression.thy
 
 
Core_Expression_Lemmas.thy
Core_Expression_Lemmas.thy
 
 
Core_Syntax.thy
Core_Syntax.thy
 
 
Eval.thy
Eval.thy
 
 
Global_Store.thy
Global_Store.thy
 
 
Micro_Rust.thy
Micro_Rust.thy
 
 
Micro_Rust_Shallow_Embedding.thy
Micro_Rust_Shallow_Embedding.thy
 
 
Micro_Rust_Shallow_Embedding_Tests.thy
Micro_Rust_Shallow_Embedding_Tests.thy
 
 
Num_Case_Expression.thy
Num_Case_Expression.thy
 
 
Numeric_Types.thy
Numeric_Types.thy
 
 
Numeric_Types_Lemmas.thy
Numeric_Types_Lemmas.thy
 
 
Option_Type.thy
Option_Type.thy
 
 
Prompts_And_Responses.thy
Prompts_And_Responses.thy
 
 
Pullback.thy
Pullback.thy
 
 
README.md
README.md
 
 
ROOT
ROOT
 
 
Range_Type.thy
Range_Type.thy
 
 
Result_Type.thy
Result_Type.thy
 
 
Rust_Iterator.thy
Rust_Iterator.thy
 
 
Rust_Iterator_Lemmas.thy
Rust_Iterator_Lemmas.thy
 
 
SSA.thy
SSA.thy
 
 
Shallow_Micro_Rust.thy
Shallow_Micro_Rust.thy
 
 
Tuple.thy
Tuple.thy
 
 

README.md

A shallow embedding of µRust

This directory contains material related to the shallow embedding of µRust (or "Micro Rust") in Isabelle/HOL.

To perform a batch build:

λ> $ISABELLE_HOME/bin/isabelle build -d ../Micro_Rust_Parsing_Frontend -D .

To open this session for interactive editing (from within the directory):

λ> $ISABELLE_HOME/bin/isabelle jedit -d ../Micro_Rust_Parsing_Frontend *.thy &