ML - MaRDI portal

Cited in

(only showing first 100 items - show all)

Efficiently checking propositional refutations in HOL theorem provers
A rewriting logic approach to operational semantics
Recasting ML\(^{\text F}\)
Adapting functional programs to higher order logic
Proof assistants: history, ideas and future
Data compression for proof replay
Using theorem proving to verify expectation and variance for discrete random variables
A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
On the existence of free models in abstract algebraic institutions
A characterization of F-complete type assignments
Toward formal development of programs from algebraic specifications: Implementations revisited
Quasi-varieties in abstract algebraic institutions
An algebraic semantics approach to the effective resolution of type equations
Pebble, a kernel language for modules and abstract data types
A semantics of multiple inheritance
Principal type scheme and unification for intersection type discipline
Polymorphic type inference and containment
On Church's formal theory of functions and functionals. The - calculus: Connections to higher type recursion theory, proof theory, category theory
Generalization from partial parametrization in higher-order type theory
Higher-order rewrite systems and their confluence
Efficient high-level parallel programming
Polymorphic syntax definition
Algebraic processing of programming languages
An efficient interpreter for the lambda-calculus
A rewrite-based type discipline for a subset of computer algebra
Co-induction in relational semantics
Type checking with universes
Static semantics, types, and binding time analysis
Modularising the specification of a small database system in extended ML
On the expressive power of finitely typed and universally polymorphic recursive procedures
\(\pi\)-RED - a graph reducer for a full-fledged \(\lambda\)-calculus
A typed functional extension of logic programming
Optimal parallel algorithms for forest and term matching
Type reconstruction in finite rank fragments of the second-order -calculus
Complete restrictions of the intersection type discipline
On subsumption and semiunification in feature algebras
Order-sorted algebra. I: Equational deduction for multiple inheritance, overloading, exceptions and partial operations
The revised report on the syntactic theories of sequential control and state
Constructing type systems over an operational semantics
Safety analysis versus type inference for partial types
On the synthesis of function inverses
Principal types of BCK-lambda-terms
Theories for mechanical proofs of imperative programs
Extending the type checker of Standard ML by polymorphic recursion
Process calculus based upon evaluation to committed form
ACL2
A behavioural theory of first-order CML
Formal verification of a programming logic for a distributed programming language
CLPS-B
Coq
Typability and type checking in System F are equivalent and undecidable
The \(HOL\) logic extended with quantification over type variables
Lazy techniques for fully expansive theorem proving
Nominalization, predication and type containment
An analysis of Böhm's theorem
A co-induction principle for recursively defined domains
Type inference with partial types
Isabelle
Deductive and inductive synthesis of equational programs
Synthesis of ML programs in the system Coq
OBSCURE, a specification language for abstract data types
Annotations in formal specifications and proofs
Ott
PCF extended with real numbers
Intersection type assignment systems
Lower bounds on type checking overloading
A note on ``A simplified account of polymorphic references
A strict functional language with cyclic recursive data
Normalization results for typeable rewrite systems
Comparing cubes of typed and type assignment systems
Full abstraction for the second order subset of an Algol-like language
TkWinHOL
TPS
Essential concepts of algebraic specification and program development
Indexed types
APL
Covariant types
The definition of Extended ML: A gentle introduction
Typed generic traversal with term rewriting strategies
Revisiting the notion of function
Modula
ALGOL 68
Encoding transition systems in sequent calculus
A linear logical framework
A rewriting approach to satisfiability procedures.
XML with data values: Typechecking revisited.
Prosper
CLEAN
Logic programs as compact denotations.
Smalltalk
Isabelle/HOL
HiLog
FoCs
Ada95
TinkerType
ArcAngel
LPTP
Design/CPN
Isabelle/Isar
FRACTRAN

This page was built for software: ML