Automating Side Conditions in Formalized Partial Functions

DOI10.1007/978-3-540-85110-3_26MaRDI QIDQ5505512zbMATH OpenOpenAlexWikidataFDO

Authors Cezary Kaliszyk

Publication date 27 January 2009

Published in Lecture Notes in Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-540-85110-3_26

Mathematics Subject Classification ID

Symbolic computation and algebraic computation (68W30)

Recommendations

• scientific article; zbMATH DE number 4074542
• Automating relatively complete verification of higher-order functional programs
• Reasoning about partial functions in the formal development of programs
• Automatic extensions of functional calculi
• Proof automation for functional correctness in separation logic
• Automated synthesis of functional programs with auxiliary functions
• Automatizing termination proofs of recursively defined functions
• Partial derivative automata formalized in Coq
• A computational formalization for partial evaluation
• scientific article; zbMATH DE number 1389654

Cites work

• Certified Computer Algebra on Top of an Interactive Theorem Prover
• First order logic with domain conditions
• scientific article; zbMATH DE number 3273551 (Why is no real title available?)
• IMPS : An interactive mathematical proof system
• Mathematical Knowledge Management
• Modelling general recursion in type theory
• Multiple-valued complex functions and computer algebra
• NIST digital library of mathematical functions
• Partial Recursive Functions in Higher-Order Logic
• USING NONSTANDARD ANALYSIS TO ENSURE THE CORRECTNESS OF SYMBOLIC COMPUTATIONS

Describes a project that uses

Uses Software

• HOL Light
• PVS
• C-CoRN
• DLMF

This page was built for publication: Automating Side Conditions in Formalized Partial Functions

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