共 26 条
[1]
Klein G(2010)seL4: formal verification of an operating-system kernel Commun. ACM 53 107-115
[2]
Andronick J(2006)A machine-checked model for a Java-like language, virtual machine, and compiler ACM Trans. Program. Lang. Syst. 28 619-695
[3]
Elphinstone K(1988)Unification in Boolean rings J. Autom. Reason. 4 381-396
[4]
Heiser G(1989)Boolean unification–the story so far J. Symb. Comput. 7 275-293
[5]
Cock D(1991)A logic programming language with lambda-abstraction, function variables, and simple unification J. Log. Comput. 1 497-536
[6]
Derrin P(1989)Equational reasoning in Isabelle Sci. Comput. Program. 12 123-149
[7]
Elkaduwe D(1989)Term rewriting and beyond–theorem proving in Isabelle Form. Asp. Comput. 1 320-338
[8]
Engelhardt K(1990)Unification in primal algebras, their powers and their varieties J. ACM 37 742-776
[9]
Kolanski R(1991)Constructive rewriting Comput. J. 34 34-41
[10]
Norrish M(1998)Winskel is (almost) right: Towards a mechanized semantics textbook Form. Asp. Comput. 10 171-186