Basin, David A. Programming Logics, MPI for Informatics, Max Planck Society;
Basin, D. A., Brown, G. M., & Leeser, M. E. (1991). Formally Verified Synthesis of Combinational CMOS Circuits. Integration: The Intern. Journal of VLSI Design, 11(3), 235-250. doi:10.1016/0167-9260(91)90048-P.