Encoding monomorphic and polymorphic types

DOI10.1007/978-3-642-36742-7_34MaRDI QIDQ5326348zbMATH OpenOpenAlexFDO

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

Mathematics Subject Classification ID

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

Cited in

(19)

• 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
• Encoding monomorphic and polymorphic types
• Iterative monomorphisation
• HOL(y)Hammer: online ATP service for HOL Light
• Efficient encodings of first-order Horn formulas in equational logic
• Extending Sledgehammer with SMT solvers
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• Handling Polymorphism in Automated Deduction
• Encoding types in ML-like languages
• A Polymorphic Vampire
• Soundly proving B method formulæ using typed sequent calculus

Describes a project that uses

Uses Software

• Why3
• MPTP 0.2
• Isabelle/HOL

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)