POPL

2012

ACM

12 years 5 months ago
2012

ACM

Despite recent successes, large-scale proof development within proof assistants remains an arcane art that is extremely timeconsuming. We argue that this can be attributed to two ...

ICFP

2010

ACM

13 years 11 months ago
2010

ACM

Modern proof assistants such as Coq and Isabelle provide high degrees of expressiveness and assurance because they support formal reasoning in higher-order logic and supply explic...

SEMWIKI

2008

13 years 11 months ago
2008

Abstract. Mathematical documents, and their instrumentation by computers, have rich structure at the layers of presentation, metadata and semantics, as objects in a system for form...

TLCA

1993

Springer

14 years 2 months ago
1993

Springer

This paper describes formalizations of Tait’s normalization proof for the simply typed λ-calculus in the proof assistants Minlog, Coq and Isabelle/HOL. From the formal proofs p...

MKM

2009

Springer

14 years 2 months ago
2009

Springer

Hilbert’s concept of formal proof is an ideal of rigour for mathematics which has important applications in mathematical logic, but seems irrelevant for the practice of mathemati...

PPDP

2007

Springer

14 years 4 months ago
2007

Springer

We describe a semantic type soundness result, formalized in the Coq proof assistant, for a compiler from a simple imperative language with heap-allocated data into an idealized as...

TPHOL

2008

IEEE

14 years 4 months ago
2008

IEEE

Although graphs are very common in computer science, they are still very difﬁcult to handle for proof assistants as proving properties of graphs may require heavy computations. T...

LICS

2008

IEEE

14 years 4 months ago
2008

IEEE

Tait’s method (a.k.a. proof by logical relations) is a powerful proof technique frequently used for showing foundational properties of languages based on typed λ-calculi. Histo...