A Representation of Fω in LF

DOI10.1016/S1571-0661(04)00280-4zbMath1268.68055OpenAlexW2049059975MaRDI QIDQ2841235

Dachuan Yu, Zhaozhong Ni, Carsten Schuermann

Publication date: 24 July 2013

Published in: Electronic Notes in Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/s1571-0661(04)00280-4

Mathematics Subject Classification ID

Functional programming and lambda calculus (68N18) Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30)

Related Items (2)

Mechanizing metatheory in a logical framework ⋮ A Representation of Fω in LF

Uses Software

• Coq
• Isabelle
• Nuprl
• Twelf
• TALx86

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Isabelle. A generic theorem prover
• A Representation of Fω in LF
• Fully reflexive intensional type analysis
• A framework for defining logics
• Stack-based typed assembly language

This page was built for publication: A Representation of Fω in LF