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

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