Вы здесь

Главная

Types for Proofs and Programs

Связанные издания:

A Concrete Final Coalgebra Theorem for ZF Set Theory
A short and flexible proof of Strong Normalization for the Calculus of Constructions
A User s Friendly Syntax to Define Recursive Functions as Typed Lambda-terms
Codifying guarded definitions with recursive schemes
Communicating Contexts: a Progmatic Approach to Information Exchange
Formalization of a Lambda-Calculus with Explicit Substitutions in Coq
I/O Automata in Isabelle/HOL
On Extensibility of Proof Checkers
Syntactic Categories in the Language of Mathematics
The Metatheory of UTT