Extension of Types-To-Sets
From MaRDI portal
- A mechanized translation from higher-order logic to set theory
- Automatic Data Refinement
- Comprehending Isabelle/HOL’s Consistency
- Constructive Type Classes in Isabelle
- Context Aware Calculation and Deduction
- From types to sets by local type definition in higher-order logic
- From types to sets by local type definitions in higher-order logic
- Interaction with formal mathematical documents in Isabelle/PIDE
- Lifting and Transfer: A Modular Design for Quotients in Isabelle/HOL
- Locales: a module system for mathematical theories
- Natural deduction as higher-order resolution
- The foundation of a generic theorem prover
- Types for Proofs and Programs
This page was built for software: Extension of Types-To-Sets
