QPC_ 2: A constructive calculus with parameterized specifications

DOI10.1016/S0747-7171(06)80008-8MaRDI QIDQ1322848zbMATH OpenFDO

Authors Yukihide Takayama

Publication date 12 January 1995

Published in Journal of Symbolic Computation (Search for Journal in Brave)

zbMATH Keywords

intuitionistic type theoryprogram extractionuniversal quantificationfunctional programsprogram synthesisprogram schemeparameterized specificationscalculus of constructionhierarchy of universessecond order constructive calculus

Mathematics Subject Classification ID

Logic programming (68N17) Specification and verification (program logics, model checking, etc.) (68Q60) Metamathematics of constructive systems (03F50) Abstract data types; algebraic specification (68Q65) Second- and higher-order arithmetic and fragments (03F35)

Recommendations

• Constructive system for automatic program synthesis
• scientific article; zbMATH DE number 2079677
• A Calculus of Higher-Order Parameterization for Algebraic Specifications
• Synthesis of ML programs in the system Coq

Cites work

• scientific article; zbMATH DE number 3910392 (Why is no real title available?)
• scientific article; zbMATH DE number 3684934 (Why is no real title available?)
• scientific article; zbMATH DE number 50149 (Why is no real title available?)
• scientific article; zbMATH DE number 3275554 (Why is no real title available?)
• Extraction of redundancy-free programs from constructive natural deduction proofs
• Formal systems for some branches of intuitionistic analysis
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Program synthesis using realizability
• Singleton, union, and intersection types for program extraction
• The calculus of constructions
• The system \({\mathcal F}\) of variable types, fifteen years later

Cited in

(2)

• QUICr: A Reusable Library for Parametric Abstraction of Sets and Numbers
• Defining concurrent processes constructively

Describes a project that uses

Uses Software

• Nuprl

This page was built for publication: \(QPC_ 2\): A constructive calculus with parameterized specifications

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