\(QPC_ 2\): A constructive calculus with parameterized specifications

DOI10.1016/S0747-7171(06)80008-8zbMath0804.68085MaRDI QIDQ1322848

Yukihide Takayama

Publication date: 12 January 1995

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

zbMATH Keywords

program extractionprogram synthesisintuitionistic type theoryuniversal quantificationfunctional programsprogram schemeparameterized specificationscalculus of constructionhierarchy of universessecond order constructive calculus

Mathematics Subject Classification ID

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

Related Items (1)

Defining concurrent processes constructively

Uses Software

• Nuprl

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Extraction of redundancy-free programs from constructive natural deduction proofs
• The system \({\mathcal F}\) of variable types, fifteen years later
• The calculus of constructions
• Program synthesis using realizability
• Singleton, union, and intersection types for program extraction
• Metamathematical investigation of intuitionistic arithmetic and analysis. With contributions by C. A. Smorynski, J. I. Zucker and W. A. Howard
• Formal systems for some branches of intuitionistic analysis

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