Cited in
(only showing first 100 items - show all)- Unifying Sets and Programs via Dependent Types
- Comprehending Isabelle/HOL’s Consistency
- On the semantics of polymorphism
- Polymorphic type inference with overloading and subtyping
- A polymorphic type system for Prolog
- Completeness and partial soundness results for intersection and union typing for \(\overline{\lambda}\mu\tilde{\mu}\)
- Proof search with set variable instantiation in the calculus of constructions
- Dependent types with subtyping and late-bound overloading
- Structuring metatheory on inductive definitions
- Type-directed specialization of polymorphism.
- Type inference for variant object types
- Source-tracking unification
- scientific article; zbMATH DE number 709076 (Why is no real title available?)
- Type system in programming languages
- Libraries for generic programming in Haskell
- A Functional Abstraction of Typed Invocation Contexts
- Essential concepts of algebraic specification and program development
- Deductive and inductive synthesis of equational programs
- Categorical ML -- category-theoretic modular programming
- From types to sets by local type definition in higher-order logic
- A functional correspondence between monadic evaluators and abstract machines for languages with computational effects
- A language for generic programming in the large
- An approach to formal verification of human-computer interaction
- Type inference with recursive types: Syntax and semantics
- Covariant types
- Unique solutions of contractions, CCS, and their HOL formalisation
- Implementing a method for stochastization of one-step processes in a computer algebra system
- High-level modelling for typed functional programming
- Correctness of compiling polymorphism to dynamic typing
- A realizability interpretation of Church's simple theory of types
- A typed resolution principle for deduction with conditional typing theory
- On the desirability of mechanizing calculational proofs
- A Scalable Inclusion Constraint Solver Using Unification
- Game theoretic analysis of call-by-value computation
- Scalable fine-grained proofs for formula processing
- Region-based memory management
- scientific article; zbMATH DE number 1231611 (Why is no real title available?)
- From types to sets by local type definitions in higher-order logic
- Proof assistance for real-time systems using an interactive theorem prover
- A cost-effective estimation of uncaught exceptions in Standard ML programs
- Satisfying subtype inequalities in polynomial space
- Open and closed scopes for constrained genericity
- Annotation inference for modular checkers
- Soundness conditions for big-step semantics
- Higher-ranked annotation polymorphic dependency analysis
- Untyping typed algebras and colouring cyclic linear logic
- Revisiting the notion of function
- Formal Analysis of Optical Waveguides in HOL
- Extended Static Checking by Calculation Using the Pointfree Transform
- Two case studies of semantics execution in Maude: CCS and LOTOS
- Principal types of BCK-lambda-terms
- Abstraction of Clocks in Synchronous Data-Flow Systems
- A concurrent logical relation
- Practical theory extension in Event-B
- Genericity and the \(\pi\)-calculus
- Unifying sets and programs via dependent types
- Intensional computation with higher-order functions
- Semantic essence of AsmL
- Principal type scheme and unification for intersection type discipline
- Programming with narrowing: a tutorial
- Term Rewriting and All That
- A co-induction principle for recursively defined domains
- Safe functional systems through integrity types and verified assembly
- A selected bibliography on constructive mathematics, intuitionistic type theory and higher order deduction
- The right tools for the job: correctness of cone of influence reduction proved using ACL2 and HOL4
- Smart testing of functional programs in Isabelle
- 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
- Proof-relevant Horn clauses for dependent type inference and term synthesis
- Complete restrictions of the intersection type discipline
- Evaluation of anonymity and confidentiality protocols using theorem proving
- 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
- Safe zero-cost coercions for Haskell
- A rewriting logic approach to operational semantics
- Towards Knowledge Management for HOL Light
- The full-reducing Krivine abstract machine KN simulates pure normal-order reduction in lockstep: a proof via corresponding calculus
- Introduction to Type Theory
- Optimal parallel algorithms for forest and term matching
- Polymorphic typed defunctionalization and concretization
- Manifest Fields and Module Mechanisms in Intensional Type Theory
- Kinded type inference for parametric overloading
- Intersection type assignment systems
- Improving type error messages for generic Java
- Theories for mechanical proofs of imperative programs
- The seven virtues of simple type theory
- Smart test data generators via logic programming
- Enhancing dependency pair method using strong computability in simply-typed term rewriting
- Using Structural Recursion for Corecursion
- Formal verification of a programming logic for a distributed programming language
- Contract-based verification of MATLAB-style matrix programs
- The correctness of Newman's typability algorithm and some of its extensions
- Evolution of rule-based programs
- Termination checking with types
- Intersection types and computational effects
- Formal analysis of the kinematic Jacobian in screw theory
- Extensional higher-order paramodulation in Leo-III
- The Imandra Automated Reasoning System (System Description)
This page was built for software: ML
