scientific article; zbMATH DE number 432706

zbMATH Open0808.03007MaRDI QIDQ3138833FDOQ3138833

Authors: Douglas J. Howe 

Publication date: 20 March 1995

Title of this publication is not available (Why is that?)

Recommendations

• scientific article; zbMATH DE number 785045
• Reflective semantics of constructive type theory
• An Essence of SSReflect
• Proof assistance for refinement in type theory
• scientific article; zbMATH DE number 2185723

zbMATH Keywords

semanticsmodified type theoryreflected proof systemreflection of proofs

Mathematics Subject Classification ID

Proof theory in general (including proof-theoretic semantics) (03F03) Mechanization of proofs and logical operations (03B35)

Cited In (11)

• Title not available (Why is that?)
• Reflection in conditional rewriting logic
• Proof reflection in Coq
• Incorporating quotation and evaluation into Church's type theory
• Reflection of formal tactics in a deductive reflection framework
• On some semantic issues in the reflective tower
• Proof-theoretic analysis by iterated reflection
• Typing in reflective combinatory logic
• Mtac: a monad for typed tactic programming in Coq
• A Logic for Reflective ASMs
• Reflective semantics of constructive type theory

Uses Software

• HOL
• 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 Q3138833)