Encoding Monomorphic and Polymorphic Types
From MaRDI portal
Publication:5326348
DOI10.1007/978-3-642-36742-7_34zbMath1381.68259OpenAlexW1526260483MaRDI QIDQ5326348
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
Lua error in Module:PublicationMSCList at line 37: attempt to index local 'msc_result' (a nil value).
Related Items (14)
Soundness and completeness proofs by coinductive methods ⋮ The higher-order prover \textsc{Leo}-II ⋮ Semi-intelligible Isar proofs from machine-generated proofs ⋮ A Polymorphic Vampire ⋮ Soundly Proving B Method Formulæ Using Typed Sequent Calculus ⋮ A learning-based fact selector for Isabelle/HOL ⋮ A formalized general theory of syntax with bindings ⋮ Encoding Monomorphic and Polymorphic Types ⋮ A formalized general theory of syntax with bindings: extended version ⋮ HOL(y)Hammer: online ATP service for HOL Light ⋮ Finding Finite Models in Multi-sorted First-Order Logic ⋮ GRUNGE: a grand unified ATP challenge ⋮ Extending Sledgehammer with SMT solvers ⋮ Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
Uses Software
This page was built for publication: Encoding Monomorphic and Polymorphic Types
