43 citations · 77 across the 16 of their papers we have counts for
Showing 2013Show all
2 papers · 1 filter
cs.LO2013★ 3 cited
Strong Normalization for HA + EM1 by Non-Deterministic Choice
Federico Aschieri
We study the strong normalization of a new Curry-Howard correspondence for HA + EM1, constructive Heyting Arithmetic with the excluded middle on Sigma01-formulas. The proof-term la…
cs.LO2013
Expansion Trees with Cut
Stefan Hetzl, Daniel Weller
Herbrand's theorem is one of the most fundamental insights in logic. From the syntactic point of view it suggests a compact representation of proofs in classical first- and higher-…