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)

• High-level modelling for typed functional programming
• On the desirability of mechanizing calculational proofs
• Formalization of Entropy Measures in HOL
• 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
• Type inference and strong static type checking for Promela
• Polar type inference with intersection types and \(\omega\)
• Simplifying proofs in Fitch-style natural deduction systems
• Formal compiler construction in a logical framework
• Programmed strategies for program verification
• Theorem Proving in Higher Order Logics
• Indexed types
• Bisimilarity is not finitely based over BPA with interrupt
• A proof-centric approach to mathematical assistants
• Formalization of the standard uniform random variable
• Logic programs as compact denotations.
• An efficient interpreter for the lambda-calculus
• Simplifying subtyping constraints: a theory
• Providing a formal linkage between MDG and HOL
• Verification of FPGA layout generators in higher-order logic
• A few exercises in theorem processing
• The Girard-Reynolds isomorphism (second edition)
• A new generic scheme for functional logic programming with constraints
• Set theory for verification. II: Induction and recursion
• A type-theoretic semantics of arrays
• Full abstraction for the second order subset of an Algol-like language
• SAC -- a functional array language for efficient multi-threaded execution
• A complete axiom system for propositional projection temporal logic with cylinder computation model
• Imperative self-adjusting computation
• Formal probabilistic analysis of detection properties in wireless sensor networks
• Pattern matching as cut elimination
• The Girard-Reynolds isomorphism
• Using theorem proving to verify expectation and variance for discrete random variables
• Meta-circular interpreter for a strongly typed language
• Constructive system for automatic program synthesis
• Pebble, a kernel language for modules and abstract data types
• On Church's formal theory of functions and functionals. The \(\lambda\)- calculus: Connections to higher type recursion theory, proof theory, category theory
• Semantics of types for database objects
• Type inference with partial types
• Co-induction in relational semantics
• A mechanical analysis of program verification strategies
• Unifying theories in ProofPower-Z
• Encoding types in ML-like languages
• Nominalization, predication and type containment
• Formal validation of pattern matching code
• Towards proving type safety of .NET CIL
• From ML to Ada: Strongly-typed language interoperability via source translation
• A logic for Miranda, revisited
• Deduction and Declarative Programming
• A consistent foundation for Isabelle/HOL
• Safety analysis versus type inference for partial types
• On the semantics of polymorphism
• Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)
• Deductive and inductive synthesis of equational programs
• A Scalable Inclusion Constraint Solver Using Unification
• Game theoretic analysis of call-by-value computation
• A language for generic programming in the large
• Extended Static Checking by Calculation Using the Pointfree Transform
• Region-based memory management
• Genericity and the \(\pi\)-calculus
• Two case studies of semantics execution in Maude: CCS and LOTOS
• Unifying sets and programs via dependent types
• Introduction to Type Theory
• 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
• Formal reliability analysis of combinational circuits using theorem proving
• Reasoning about conditional probabilities in a higher-order-logic theorem prover
• A rewriting logic approach to operational semantics
• Improving type error messages for generic Java
• The correctness of Newman's typability algorithm and some of its extensions
• Title not available (Why is that?)
• Title not available (Why is that?)
• Typed generic traversal with term rewriting strategies
• Combining Decision Procedures by (Model-)Equality Propagation
• Parametric higher-order abstract syntax for mechanized semantics
• On the existence of free models in abstract algebraic institutions
• XML with data values: Typechecking revisited.
• Higher-order rewrite systems and their confluence
• MetaML and multi-stage programming with explicit annotations
• A framework for the verification of certifying computations
• Mechanised support for sound refinement tactics
• Curry-Howard for incomplete first-order logic derivations using one-and-a-half level terms
• Monotonicity inference for higher-order formulas
• Computability in higher types, P\(\omega\) and the completeness of type assignment
• Forum: A multiple-conclusion specification logic
• The locally nameless representation
• Recasting ML\(^{\text F}\)
• A characterization of F-complete type assignments
• Completeness of type assignment in continuous lambda models
• Polymorphic type inference and containment
• Exploring structural symmetry automatically in symbolic trajectory evaluation
• An algebraic semantics approach to the effective resolution of type equations
• Implicit propagation in structural operational semantics
• An analysis of Böhm's theorem

This page was built for software: ML