scientific article; zbMATH DE number 1223720

zbMath0910.03022MaRDI QIDQ4219036

Eduardo Giménez

Publication date: 15 November 1998

Title: zbMATH Open Web Interface contents unavailable due to conflicting licenses.

zbMATH Keywords

normalizationextension of the Calculus of Construction with inductive and co-inductive typesrepresentation of recursive programs in type theory

Mathematics Subject Classification ID

Logic in computer science (03B70) Second- and higher-order arithmetic and fragments (03F35)

Related Items (13)

Trace-Based Coinductive Operational Semantics for While ⋮ Size-based termination of higher-order rewriting ⋮ Is sized typing for Coq practical? ⋮ Termination of rewrite relations on \(\lambda\)-terms based on Girard's notion of reducibility ⋮ Interactive programming in Agda – Objects and graphical user interfaces ⋮ Type-based termination of generic programs ⋮ Termination checking with types ⋮ Recursive coalgebras from comonads ⋮ A Tutorial on Type-Based Termination ⋮ A metalanguage for guarded iteration ⋮ Least and greatest fixed points in intuitionistic natural deduction ⋮ Corecursion and Non-divergence in Session-Typed Processes ⋮ Adapting functional programs to higher order logic

This page was built for publication: