21 citations · 39 across the 3 of their papers we have counts for
3 papers
math.NA2016★ 4 cited
Semantics, Specification Logic, and Hoare Logic of Exact Real Computation
Sewon Park, Franz Brauße, Pieter Collins +7
We propose a simple imperative programming language, ERC, that features arbitrary real numbers as primitive data type, exactly. Equipped with a denotational semantics, ERC provides…
cs.LO2011★ 14 cited
Proof-irrelevant model of CC with predicative induction and judgmental equality
Gyesik Lee, Benjamin Werner
We present a set-theoretic, proof-irrelevant model for Calculus of Constructions (CC) with predicative induction and judgmental equality in Zermelo-Fraenkel set theory with an axio…
math.LO2009★ 21 cited
Kripke Models for Classical Logic
Danko Ilik, Gyesik Lee, Hugo Herbelin
We introduce a notion of Kripke model for classical logic for which we constructively prove soundness and cut-free completeness. We discuss the novelty of the notion and its potent…