Sciweavers

POPL
2012
ACM
12 years 5 months ago
Static and user-extensible proof checking
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 ...
Antonis Stampoulis, Zhong Shao
ICFP
2010
ACM
13 years 11 months ago
VeriML: typed computation of logical terms inside a language with effects
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...
Antonis Stampoulis, Zhong Shao
SEMWIKI
2008
134views Data Mining» more  SEMWIKI 2008»
13 years 11 months ago
A Real Semantic Web for Mathematics Deserves a Real Semantics
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...
Cezary Kaliszyk, Pierre Corbineau, Freek Wiedijk, ...
TLCA
1993
Springer
14 years 2 months ago
Program Extraction from Normalization Proofs
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...
Ulrich Berger
MKM
2009
Springer
14 years 2 months ago
Formal Proof: Reconciling Correctness and Understanding
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...
Cristian S. Calude, Christine Müller
PPDP
2007
Springer
14 years 4 months ago
Formalizing and verifying semantic type soundness of a simple compiler
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...
Nick Benton, Uri Zarfaty
TPHOL
2008
IEEE
14 years 4 months ago
Certifying a Termination Criterion Based on Graphs, without Graphs
Although graphs are very common in computer science, they are still very difficult to handle for proof assistants as proving properties of graphs may require heavy computations. T...
Pierre Courtieu, Julien Forest, Xavier Urbain
LICS
2008
IEEE
14 years 4 months ago
Structural Logical Relations
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...
Carsten Schürmann, Jeffrey Sarnat