scientific article; zbMATH DE number 432706

MaRDI QIDQ3138833zbMATH OpenFDO

Authors Douglas J. Howe

Publication date 20 March 1995

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)

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

Cited in

(11)

• scientific article; zbMATH DE number 2185723 (Why is no real title available?)
• 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

Describes a project that uses

Uses Software

• Nuprl
• HOL

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)