3 citations · 4 across the 3 of their papers we have counts for
Showing cs.LOShow all
2 papers · 1 filter
cs.LO2018
Formalisation of a frame stack semantics for a Java-like language
Aleksy Schubert, Jacek Chrząszcz
We present a Coq formalisation of the small-step operational semantics of Jafun, a small Java-like language with classes. This format of semantics makes it possible to naturally sp…
cs.LO2008★ 3 cited
Consistency and Completeness of Rewriting in the Calculus of Constructions
Daria Walukiewicz-Chrzaszcz, Jacek Chrzaszcz
Adding rewriting to a proof assistant based on the Curry-Howard isomorphism, such as Coq, may greatly improve usability of the tool. Unfortunately adding an arbitrary set of rewrit…