ML
From MaRDI portal
Software:13958
No author found.
Related Items (only showing first 100 items - show all)
Contract-based verification of MATLAB-style matrix programs ⋮ 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 ⋮ High-level modelling for typed functional programming ⋮ Efficient virtual machine support of runtime structural reflection ⋮ Proof pearl: Mechanizing the textbook proof of Huffman's algorithm ⋮ Compilation of extended recursion in call-by-value functional languages ⋮ Simplifying proofs in Fitch-style natural deduction systems ⋮ Ordinal arithmetic: Algorithms and mechanization ⋮ Polymorphic typed defunctionalization and concretization ⋮ Formal compiler construction in a logical framework ⋮ Formalization of reliability block diagrams in higher-order logic ⋮ Effect-polymorphic behaviour inference for deadlock checking ⋮ Type checking a multithreaded functional language with session types ⋮ Bisimilarity is not finitely based over BPA with interrupt ⋮ Functorial semantics of first-order views ⋮ Deciding Boolean algebra with Presburger arithmetic ⋮ TPS: A hybrid automatic-interactive system for developing proofs ⋮ A proof-centric approach to mathematical assistants ⋮ Computer supported mathematics with \(\Omega\)MEGA ⋮ SAD as a mathematical assistant -- how should we go from here to there? ⋮ A two-valued logic for properties of strict functional programs allowing partial functions ⋮ Database query languages and functional logic programming ⋮ Verification of FPGA layout generators in higher-order logic ⋮ Providing a formal linkage between MDG and HOL ⋮ Generating meta-heuristic optimization code using ADATE ⋮ The Girard-Reynolds isomorphism (second edition) ⋮ A few exercises in theorem processing ⋮ A new generic scheme for functional logic programming with constraints ⋮ An approach for lifetime reliability analysis using theorem proving ⋮ Semantic types and approximation for Featherweight Java ⋮ An observationally complete program logic for imperative higher-order functions ⋮ Full abstraction for Reduced ML ⋮ Unifying sets and programs via dependent types ⋮ A complete axiom system for propositional projection temporal logic with cylinder computation model ⋮ Specifying rewrite strategies for interactive exercises ⋮ Formal probabilistic analysis of detection properties in wireless sensor networks ⋮ Mechanised support for sound refinement tactics ⋮ Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\) ⋮ Meta-circular interpreter for a strongly typed language ⋮ Monotonicity inference for higher-order formulas ⋮ Analytic tableaux for higher-order logic with choice ⋮ Constructive system for automatic program synthesis ⋮ Deforestation: Transforming programs to eliminate trees ⋮ Semantics of types for database objects ⋮ Type inference for polymorphic references ⋮ Exploring structural symmetry automatically in symbolic trajectory evaluation ⋮ The calculus of context relations ⋮ Core FOBS: A hybrid functional and object-oriented language ⋮ Automatic verification of reduction techniques in higher order logic ⋮ An inductive approach to strand spaces ⋮ Linearity and iterator types for Gödel's system \(\mathcal T\) ⋮ A mechanical analysis of program verification strategies ⋮ Formal analysis of optical systems ⋮ Extending FeatherTrait Java with interfaces ⋮ Programming with algebraic effects and handlers ⋮ Towards proving type safety of .NET CIL ⋮ Forum: A multiple-conclusion specification logic ⋮ From CML to its process algebra ⋮ The complexity of higher-order queries ⋮ Term rewriting and Hoare logic -- Coded rewriting ⋮ Precedences in specifications and implementations of programming languages ⋮ Proof synthesis and reflection for linear arithmetic ⋮ On the role of memory in object-based and object-oriented languages ⋮ Mapping a functional notation for parallel programs onto hypercubes ⋮ The seven virtues of simple type theory ⋮ Reusing and modifying rulebases by predicate substitution ⋮ Region-based memory management ⋮ Categorical ML -- category-theoretic modular programming ⋮ Computational interpretations of linear logic ⋮ An approach to completing variable names for implicitly typed functional languages ⋮ On graph rewriting, reduction, and evaluation in the presence of cycles ⋮ A language for generic programming in the large ⋮ Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms ⋮ Polymorphic type inference for the relational algebra ⋮ The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4 ⋮ A novel formalization of symbolic trajectory evaluation semantics in Isabelle/HOL ⋮ Programming with narrowing: a tutorial ⋮ Reasoning about conditional probabilities in a higher-order-logic theorem prover ⋮ Formal reliability analysis of combinational circuits using theorem proving ⋮ The correctness of Newman's typability algorithm and some of its extensions ⋮ Interactive theorem proving and program development. Coq'Art: the calculus of inductive constructions. Foreword by Gérard Huet and Christine Paulin-Mohring. ⋮ Computability in higher types, P\(\omega\) and the completeness of type assignment ⋮ Exception tracking in an open world ⋮ Continuous KAOS, ASM, and formal control system design across the continuous/discrete modeling interface: a simple train stopping application ⋮ N. G. de Bruijn's contribution to the formalization of mathematics ⋮ Implementing geometric algebra products with binary trees ⋮ The semantics of second-order lambda calculus ⋮ Type inference with recursive types: Syntax and semantics ⋮ Strong normalization of \(\mathsf{ML}^{\mathsf F}\) via a calculus of coercions ⋮ Bio-PEPAd: a non-Markovian extension of Bio-PEPA ⋮ Formal reliability and failure analysis of Ethernet based communication networks in a smart grid substation ⋮ Completeness of type assignment in continuous lambda models ⋮ A polymorphic type system for Prolog ⋮ Type inference for record concatenation and multiple inheritance ⋮ Logic-based subsumption architecture ⋮ A complete mechanization of correctness of a string-preprocessing algorithm ⋮ Two case studies of semantics execution in Maude: CCS and LOTOS ⋮ Formalization of fixed-point arithmetic in HOL
This page was built for software: ML
