Encoding monomorphic and polymorphic types

DOI10.1007/978-3-642-36742-7_34zbMATH Open1381.68259OpenAlexW1526260483MaRDI QIDQ5326348FDOQ5326348

Authors: Jasmin Christian Blanchette, Sascha Böhme, Andrei Popescu, Nicholas Smallbone 

Publication date: 5 August 2013

Published in: Tools and Algorithms for the Construction and Analysis of Systems (Search for Journal in Brave)

Full work available at URL: https://eprints.mdx.ac.uk/15166/1/TACAS2013.pdf

Recommendations

• Encoding monomorphic and polymorphic types
• Optimized encodings of fragments of type theory in first order logic
• Expressing polymorphic types in a many-sorted language
• Handling Polymorphism in Automated Deduction
• TFF1: The TPTP Typed First-Order Form with Rank-1 Polymorphism

Mathematics Subject Classification ID

Cited In (17)

• Soundly Proving B Method Formulæ Using Typed Sequent Calculus
• A formalized general theory of syntax with bindings
• The higher-order prover \textsc{Leo}-II
• Semi-intelligible Isar proofs from machine-generated proofs
• A formalized general theory of syntax with bindings: extended version
• Expressing polymorphic types in a many-sorted language
• Soundness and completeness proofs by coinductive methods
• GRUNGE: a grand unified ATP challenge
• Finding Finite Models in Multi-sorted First-Order Logic
• A learning-based fact selector for Isabelle/HOL
• HOL(y)Hammer: online ATP service for HOL Light
• Extending Sledgehammer with SMT solvers
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Handling Polymorphism in Automated Deduction
• Encoding Monomorphic and Polymorphic Types
• Encoding types in ML-like languages
• A Polymorphic Vampire

Uses Software

• Isabelle/HOL
• MPTP 0.2
• Why3

This page was built for publication: Encoding monomorphic and polymorphic types

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