Skip to main content
Disciplines
Automotive Business IT + Informatics Construction + Real Estate Electrical Engineering + Electronics Energy + Sustainability Insurance + Risk Finance + Banking Management + Leadership Marketing + Sales Mechanical Engineering + Materials
Events
DE
EN
Books
Journals
Topic Page
Marketing
Start single access now
Access for companies
EXTENDED SEARCH
Log in
Top

Journal of Automated Reasoning

Issue 3/2012

Special Issue: The POPLmark Challenge

Content (7 Articles)

Preface

Benjamin C. Pierce, Stephanie Weirich

A Solution to the PoplMark Challenge Using de Bruijn Indices in Isabelle/HOL

Stefan Berghofer

A Solution to the PoplMark Challenge Based on de Bruijn Indices

Jérôme Vouillon

The Locally Nameless Representation

Arthur Charguéraud

Nested Abstract Syntax in Coq

André Hirschowitz, Marco Maggesi

Formal Metatheory of Programming Languages in the Matita Interactive Theorem Prover

Andrea Asperti, Wilmer Ricciotti, Claudio Sacerdoti Coen, Enrico Tassi

A List-Machine Benchmark for Mechanized Metatheory

Andrew W. Appel, Robert Dockins, Xavier Leroy

Aug 12
Issue: 2/2012
Special Issue: Theory and Applications of Abstraction, Substitution and Naming
Dec 12
Issue: 4/2012

Current Publications

scroll for more

use your arrow keys for more

scroll or use arrow keys for more

Premium Partner

    Image Credits