Open palmskog opened 4 years ago
The BIR language and its semantics could be worth specifying and documenting standalone, most directly using Lem. Encoding BIR in Lem would also allow porting it to other proof assistants like Isabelle/HOL and Coq.
The BIR language and its semantics could be worth specifying and documenting standalone, most directly using Lem. Encoding BIR in Lem would also allow porting it to other proof assistants like Isabelle/HOL and Coq.