scientific article; zbMATH DE number 785045

MaRDI QIDQ4842534zbMATH OpenFDO

Authors Robert Constable

Publication date 13 February 1996

zbMATH Keywords

decision proceduresNuprl proverproblem solving environments

Mathematics Subject Classification ID

Problem solving in the context of artificial intelligence (heuristics, search strategies, etc.) (68T20)

Recommendations

• Reflective semantics of constructive type theory
• An effective theory of type refinements
• Typing in reflective combinatory logic
• Explaining type inference
• scientific article; zbMATH DE number 1265030
• scientific article; zbMATH DE number 2064184
• A type system for reflective program generators
• Refining inductive types
• In the Search of a Naive Type Theory
• Fully reflexive intensional type analysis

Cited in

(6)

• Incorporating quotation and evaluation into Church's type theory
• Proof-producing reflection for HOL. With an application to model polymorphism
• scientific article; zbMATH DE number 432706 (Why is no real title available?)
• scientific article; zbMATH DE number 1341617 (Why is no real title available?)
• Theorem Proving in Higher Order Logics
• Directly reflective meta-programming

Describes a project that uses

Uses Software

• Nuprl

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 Q4842534)