scientific article; zbMATH DE number 785045

MaRDI QIDQ4842534zbMATH OpenFDO

Authors Robert Constable

Publication date 13 February 1996

zbMATH Keywords

decision proceduresproblem solving environmentsNuprl prover

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

(5)

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

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)