ML

swMATH1218MaRDI QIDQ13958FDOQ13958

Author name not available (Why is that?)

Described by source

• A theory of type polymorphism in programming
• Unnamed Publication
• Unnamed Publication
• Unnamed Publication

Cited In (only showing first 100 items - show all)

• Essential concepts of algebraic specification and program development
• Compressing Propositional Refutations
• Formal Analysis of Optical Waveguides in HOL
• Term Rewriting and All That
• Semantic essence of AsmL
• Principal type scheme and unification for intersection type discipline
• Towards Knowledge Management for HOL Light
• Complete restrictions of the intersection type discipline
• Intersection type assignment systems
• Enhancing dependency pair method using strong computability in simply-typed term rewriting
• Computer Aided Verification
• Contract-based verification of MATLAB-style matrix programs
• A decision procedure for linear ``big O equations
• Friends with Benefits
• Computational interpretations of linear logic
• Title not available (Why is that?)
• Title not available (Why is that?)
• PCF extended with real numbers
• A Brief Overview of HOL4
• The higher-order prover \textsc{Leo}-II
• Semi-intelligible Isar proofs from machine-generated proofs
• Self-formalisation of higher-order logic. Semantics, soundness, and a verified implementation
• The Orc Programming Language
• An observationally complete program logic for imperative higher-order functions
• Game-theoretic analysis of call-by-value computation
• A semantics of multiple inheritance
• Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
• Typability and type checking in System F are equivalent and undecidable
• Coalgebraic minimization of HD-automata for the \(\pi\)-calculus using polymorphic types
• Computer supported mathematics with \(\Omega\)MEGA
• The revised report on the syntactic theories of sequential control and state
• Modular structural operational semantics
• Polymorphic type inference for the relational algebra
• Proof synthesis and reflection for linear arithmetic
• Efficiently checking propositional refutations in HOL theorem provers
• Deforestation: Transforming programs to eliminate trees
• Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring.
• Nominal unification
• Principality and type inference for intersection types using expansion variables
• Predicate logic as a modeling language: modeling and solving some machine learning and data mining problems withIDP3
• Formal analysis of optical systems
• Operational reasoning for functions with local state
• Polymorphic type-checking for the ramified theory of types of Principia Mathematica
• A rewriting approach to satisfiability procedures.
• Evaluating general purpose automated theorem proving systems
• VeriML
• Formalization of reliability block diagrams in higher-order logic
• Effect-polymorphic behaviour inference for deadlock checking
• Reconstruction of Z3's bit-vector proofs in HOL4 and Isabelle/HOL
• Preface to the special issue: Interactive theorem proving and the formalization of mathematics
• Formalisation in higher-order logic and code generation to functional languages of the Gauss-Jordan algorithm
• A structural approach to reversible computation
• Analytic tableaux for higher-order logic with choice
• Towards the Formal Reliability Analysis of Oil and Gas Pipelines
• TPS: A theorem-proving system for classical type theory
• Core FOBS: A hybrid functional and object-oriented language
• Generating meta-heuristic optimization code using ADATE
• HOL(y)Hammer: online ATP service for HOL Light
• Practical affine types
• Full Abstraction for Reduced ML
• Functorial semantics of first-order views
• Programming with algebraic effects and handlers
• Quasi-varieties in abstract algebraic institutions
• A two-valued logic for properties of strict functional programs allowing partial functions
• TPS: A hybrid automatic-interactive system for developing proofs
• SAD as a mathematical assistant -- how should we go from here to there?
• An Effect System for Algebraic Effects and Handlers
• Psi-calculi in Isabelle
• The Watson theorem prover
• Learning-assisted automated reasoning with \(\mathsf{Flyspeck}\)
• On the formalization of gamma function in HOL
• Formalizing Bachmair and Ganzinger's ordered resolution prover
• Compilation of extended recursion in call-by-value functional languages
• A Compiled Implementation of Normalization by Evaluation
• Translating higher-order clauses to first-order clauses
• An overview of the K semantic framework
• OBSCURE, a specification language for abstract data types
• Comparing cubes of typed and type assignment systems
• Mechanized semantics for the clight subset of the C language
• Partial and nested recursive function definitions in higher-order logic
• Proof-producing translation of higher-order logic into pure and stateful ML
• Verified Efficient Implementation of Gabow’s Strongly Connected Component Algorithm
• Programming with binders and indexed data-types
• Fixpoints and search in PVS
• The definition of Extended ML: A gentle introduction
• Automatic proof and disproof in Isabelle/HOL
• Synthesis of ML programs in the system Coq
• HOL Light: An Overview
• Normalization results for typeable rewrite systems
• Toward formal development of programs from algebraic specifications: Implementations revisited
• High-level modelling for typed functional programming
• On the desirability of mechanizing calculational proofs
• Programming with narrowing: a tutorial
• Efficient virtual machine support of runtime structural reflection
• Proof pearl: Mechanizing the textbook proof of Huffman's algorithm
• Adapting functional programs to higher order logic
• Hybrid interactive theorem proving using nuprl and HOL
• Termination checking with types
• A constraint-based region inference algorithm
• A typed context calculus

This page was built for software: ML