| Home |
| About |
| Submission |
| Updating Entries |
| Using Entries |
| Search |
| Statistics |
| Index |
| Download |
Extension of Types-To-Sets
| Title: | Extension of Types-To-Sets |
| Author: | Mihails Milehins |
| Submission date: | 2021-09-06 |
| Abstract: | In their article titled From Types to Sets by Local Type Definitions in Higher-Order Logic and published in the proceedings of the conference Interactive Theorem Proving in 2016, Ondřej Kunčar and Andrei Popescu propose an extension of the logic Isabelle/HOL and an associated algorithm for the relativization of the type-based theorems to more flexible set-based theorems, collectively referred to as Types-To-Sets. One of the aims of their work was to open an opportunity for the development of a software tool for applied relativization in the implementation of the logic Isabelle/HOL of the proof assistant Isabelle. In this article, we provide a prototype of a software framework for the interactive automated relativization of theorems in Isabelle/HOL, developed as an extension of the proof language Isabelle/Isar. The software framework incorporates the implementation of the proposed extension of the logic, and builds upon some of the ideas for further work expressed in the original article on Types-To-Sets by Ondřej Kunčar and Andrei Popescu and the subsequent article Smooth Manifolds and Types to Sets for Linear Algebra in Isabelle/HOL that was written by Fabian Immler and Bohua Zhan and published in the proceedings of the International Conference on Certified Programs and Proofs in 2019. |
| BibTeX: |
@article{Types_To_Sets_Extension-AFP,
author = {Mihails Milehins},
title = {Extension of Types-To-Sets},
journal = {Archive of Formal Proofs},
month = sep,
year = 2021,
note = {\url{https://isa-afp.org/entries/Types_To_Sets_Extension.html},
Formal proof development},
ISSN = {2150-914x},
}
|
| License: | BSD License |
| Depends on: | Conditional_Transfer_Rule |
|
Proof outline Proof document |
| Browse theories |
| Download this entry |
| Older releases: None |