Proceedings of the Eighth ACM SIGPLAN international workshop on Logical frameworks & meta-languages: theory & practice - LFMTP '13
Latest Publications

TOTAL DOCUMENTS

(FIVE YEARS 0)

H-INDEX

(FIVE YEARS 0)

Published By ACM Press

9781450323826

Latest Documents Most Cited Documents Contributed Authors Related Sources Related Keywords

Foundational proof certificates

Proceedings of the Eighth ACM SIGPLAN international workshop on Logical frameworks & meta-languages: theory & practice - LFMTP '13 ◽

10.1145/2503887.2503894 ◽

2013 ◽

Cited By ~ 2

Author(s):

Dale Miller

Download Full-text

Towards extracting explicit proofs from totality checking in twelf

Proceedings of the Eighth ACM SIGPLAN international workshop on Logical frameworks & meta-languages: theory & practice - LFMTP '13 ◽

10.1145/2503887.2503893 ◽

2013 ◽

Cited By ~ 3

Author(s):

Yuting Wang ◽

Gopalan Nadathur

Download Full-text

Explicit convertibility proofs in pure type systems

Proceedings of the Eighth ACM SIGPLAN international workshop on Logical frameworks & meta-languages: theory & practice - LFMTP '13 ◽

10.1145/2503887.2503890 ◽

2013 ◽

Cited By ~ 7

Author(s):

Floris van Doorn ◽

Herman Geuvers ◽

Freek Wiedijk

Keyword(s):

Type Systems ◽

Pure Type ◽

Pure Type Systems

Download Full-text

Structural logical relations with case analysis and equality reasoning

Proceedings of the Eighth ACM SIGPLAN international workshop on Logical frameworks & meta-languages: theory & practice - LFMTP '13 ◽

10.1145/2503887.2503891 ◽

2013 ◽

Cited By ~ 3

Author(s):

Ulrik Rasmussen ◽

Andrzej Filinski

Keyword(s):

Case Analysis ◽

Equality Reasoning

Download Full-text

First-class substitutions in contextual type theory

Proceedings of the Eighth ACM SIGPLAN international workshop on Logical frameworks & meta-languages: theory & practice - LFMTP '13 ◽

10.1145/2503887.2503889 ◽

2013 ◽

Cited By ~ 7

Author(s):

Andrew Cave ◽

Brigitte Pientka

Keyword(s):

Type Theory

Download Full-text

A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus

Proceedings of the Eighth ACM SIGPLAN international workshop on Logical frameworks & meta-languages: theory & practice - LFMTP '13 ◽

10.1145/2503887.2503892 ◽

2013 ◽

Cited By ~ 3

Author(s):

Mahfuza Farooque ◽

Stéphane Graham-Lengrand ◽

Assia Mahboubi

Keyword(s):

Search Strategy ◽

Sequent Calculus ◽

Proof Search

Download Full-text

25 years of formal proof cultures

Proceedings of the Eighth ACM SIGPLAN international workshop on Logical frameworks & meta-languages: theory & practice - LFMTP '13 ◽

10.1145/2503887.2503896 ◽

2013 ◽

Cited By ~ 2

Author(s):

Furio Honsell

Keyword(s):

Formal Proof

Download Full-text

Proceedings of the Eighth ACM SIGPLAN international workshop on Logical frameworks & meta-languages: theory & practice - LFMTP '13Latest Publications

TOTAL DOCUMENTS

H-INDEX

Published By ACM Press

Foundational proof certificates

Towards extracting explicit proofs from totality checking in twelf

Explicit convertibility proofs in pure type systems

Structural logical relations with case analysis and equality reasoning

First-class substitutions in contextual type theory

A bisimulation between DPLL(T) and a proof-search strategy for the focused sequent calculus

25 years of formal proof cultures

Proceedings of the Eighth ACM SIGPLAN international workshop on Logical frameworks & meta-languages: theory & practice - LFMTP '13
Latest Publications