Expressiveness + Automation + Soundness: Towards Combining SMT Solvers and Interactive Proof Assistants.

Pascal Fontaine, Jean-Yves Marion, Stephan Merz, Leonor Prensa Nieto, Alwen Fernanto Tiu

Browse the full TACAS paper archive.