Return to Article Details LF+ in Coq for "fast and loose" reasoning Download Download PDF