scientific article; zbMATH DE number 1400716

MaRDI QIDQ4939698zbMATH OpenFDO

Authors Herman Geuvers, Mark-Jan Nederhof

Publication date 9 February 2000

Mathematics Subject Classification ID

Combinatory logic and lambda calculus (03B40) Logic in computer science (03B70) Functional programming and lambda calculus (68N18) Semantics in the theory of computing (68Q55)

Cited in

(14)

• On the adequacy of representing higher order intuitionistic logic as a pure type system
• Comparing cubes of typed and type assignment systems
• A higher-order calculus and theory abstraction
• Modularity of termination and confluence in combinations of rewrite systems with _
• Modular properties of algebraic type systems
• A simple model construction for the calculus of constructions
• Weak normalization implies strong normalization in a class of non-dependent pure type systems
• An induction principle for pure type systems
• Checking algorithms for Pure Type Systems
• Closure under alpha-conversion
• A short and flexible proof of strong normalization for the calculus of constructions
• Encoding Agda programs using rewriting
• A shallow embedding of pure type systems into first-order logic
• Interacting safely with an unsafe environment

This page was built for publication:

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q4939698)