6 citations · 15 across the 9 of their papers we have counts for
Showing 2018Show all
3 papers · 1 filter
cs.LO2018★ 2 cited
Concrete Semantics with Coq and CoqHammer
Łukasz Czajka, Burak Ekici, Cezary Kaliszyk
The "Concrete Semantics" book gives an introduction to imperative programming languages accompanied by an Isabelle/HOL formalization. In this paper we discuss a re-formalization of…
cs.LO2018★ 2 cited
A new coinductive confluence proof for infinitary lambda calculus
Łukasz Czajka
We present a new and formal coinductive proof of confluence and normalisation of Böhm reduction in infinitary lambda calculus. The proof is simpler than previous proofs of this res…
cs.LO2018
An operational interpretation of coinductive types
Łukasz Czajka
We introduce an operational rewriting-based semantics for strictly positive nested higher-order (co)inductive types. The semantics takes into account the "limits" of infinite reduc…