Re: [isabelle] Isabelle functions: Always total, sometimes undefined



Surely the point is that Coq (or rather its underlying calculus, and similar type theories) have an operational semantics. The semantics of higher-order logic is set-theoretic. Therefore higher-order logic has no definitive operational semantics at all. Rather we identify an executable sublanguage.

Larry Paulson



> On 19 Oct 2017, at 10:30, Florian Haftmann <florian.haftmann at informatik.tu-muenchen.de> wrote:
> 
> e) Why there is nothing but a quite loose characterization of the
> Âexecutable sublanguage of Isabelle/HOL.
> 
> It is the sheer complexity of the system itself: The sublanguage is not
> built into the logic, but appears by a elaborate stack of tools:
> 




This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.