Encoding Monomorphic and Polymorphic Types

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

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

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

Cited In (15)

• 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
• 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}\)
• 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)