Search results for "MERLIN"

Hits ?▲	Authors	Title	Venue	Year	Link	Author keywords
1	Marino Miculan, Ivan Scagnetto, Furio Honsell	Translating specifications from nominal logic to CIC with the theory of contexts.	MERLIN	2005	DBLP DOI BibTeX RDF	calculus of inductive constructions, languages with binders, logical expressivity, theory of contexts, nominal logics
1	Miki Tanaka, John Power	A unified category-theoretic formulation of typed binding signatures.	MERLIN	2005	DBLP DOI BibTeX RDF	binding signature, pseudo-distributive law, substitution monoidal structure, variable binding, pseudo-monad
1	Aleksey Nogin, Alexei Kopylov, Xin Yu, Jason Hickey	A computational approach to reflective meta-reasoning about languages with bindings.	MERLIN	2005	DBLP DOI BibTeX RDF	MetaPRL, Nuprl, languages with bindings, programming language, reflection, experimentation, type theory, higher-order abstract syntax
1	Christian Urban, Michael Norrish	A formal treatment of the barendregt variable convention in rule inductions.	MERLIN	2005	DBLP DOI BibTeX RDF	POPLmark challenge, ?-calculus, nominal logic
1	Randy Pollack (eds.)	ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2005, Tallinn, Estonia, September 30, 2005	MERLIN	2005	DBLP DOI BibTeX RDF
1	Olha Shkaravska	Types with semantics: soundness proof assistant.	MERLIN	2005	DBLP DOI BibTeX RDF	type system, assertion, automated theorem proving, program logic
1	James Cheney	Toward a general theory of names: binding and scope.	MERLIN	2005	DBLP DOI BibTeX RDF	names, abstract syntax, scope, nominal logic
1	Frank Pfenning	Towards a type theory of contexts.	MERLIN	2005	DBLP DOI BibTeX RDF
1	Kevin Donnelly, Hongwei Xi	Combining higher-order abstract syntax with first-order abstract syntax in ATS.	MERLIN	2005	DBLP DOI BibTeX RDF	ATS/LF, theorem proving, dependent types, higher-order abstract syntax, ATS
1	Alberto Ciaffaglione, Luigi Liquori, Marino Miculan	Reasoning on an imperative object-based calculus in Higher Order Abstract Syntax.	MERLIN	2003	DBLP DOI BibTeX RDF	logical foundations of programming, object-based calculi with side-effects, program and system verification, logical frameworks, interactive theorem proving
1	John Power	A unified category theoretic approach to variable binding.	MERLIN	2003	DBLP DOI BibTeX RDF	binding signature, pseudo-distributive law, substitution monoidal structure, variable binding, pseudo-monad
1	Michael Norrish	Mechanising Hankin and Barendregt using the Gordon-Melham axioms.	MERLIN	2003	DBLP DOI BibTeX RDF	higher order abstract syntax, interactive theorem-proving
1	Aleksandar Nanevski, Brigitte Pientka, Frank Pfenning	A modal foundation for meta-variables.	MERLIN	2003	DBLP DOI BibTeX RDF	modal type theory, pattern unification, logical frameworks
1		Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2003, Uppsala, Sweden, August 2003	MERLIN	2003	DBLP DOI BibTeX RDF
1	Alberto Momigliano, Jeff Polakow	A formalization of an Ordered Logical Framework in Hybrid with applications to continuation machines.	MERLIN	2003	DBLP DOI BibTeX RDF	continuation machines, ordered linear logic, logical frameworks, higher order abstract syntax
1	S. J. Ambler, Roy L. Crole, Alberto Momigliano	A definitional approach to primitivexs recursion over higher order abstract syntax.	MERLIN	2003	DBLP DOI BibTeX RDF	Isabelle HOL, topos theory, ?-calculus, higher order abstract syntax, primitive recursion, initial algebras
1	Neil Ghani, Tarmo Uustalu	Explicit substitutions and higher-order syntax.	MERLIN	2003	DBLP DOI BibTeX RDF	algebras, monads, abstract syntax, explicit substitutions, variable binding
1	Ralph-Johan Back, Viorel Preoteasa	Reasoning about recursive procedures with parameters.	MERLIN	2003	DBLP DOI BibTeX RDF	predicate transformer semantics, Hoare logic, refinement calculus, recursive procedures
1	Carsten Schürmann, Jatin Shah	Representing reductions of NP-complete problems in logical frameworks: a case study.	MERLIN	2003	DBLP DOI BibTeX RDF	linear logic, NP-complete problems, logical frameworks
1	Yasuhiko Minamide, Koji Okuma	Verifying CPS transformations in Isabelle/HOL.	MERLIN	2003	DBLP DOI BibTeX RDF	program transformation, theorem proving, correctness proofs
1	Jason Hickey, Aleksey Nogin, Adam Granicz	Compiler implementation in a formal logical framework.	MERLIN	2003	DBLP DOI BibTeX RDF	formal compiler, higher-order abstract syntax, logical programming environment
1	Christine Röckl	A First-Order Syntax for the Pi-Calculus in Isabelle/HOL using Permutations.	MERLIN	2001	DBLP DOI BibTeX RDF
1	Carsten Schürmann, Dachuan Yu, Zhaozhong Ni	A Representation of Fomega in LF.	MERLIN	2001	DBLP DOI BibTeX RDF
1	Marino Miculan	Developing (Meta)Theory of Lambda-calculus in the Theory of Context.	MERLIN	2001	DBLP DOI BibTeX RDF
1	Andreas Abel 0001	A Third-Order Representation of the lambda-mu-Calculus.	MERLIN	2001	DBLP DOI BibTeX RDF
1	René Vestergaard, James Brotherston	The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective).	MERLIN	2001	DBLP DOI BibTeX RDF
1	Simon Ambler, Roy L. Crole, Alberto Momigliano	Preface: Mechanised Reasoning about Languages with Variable Binding 2001.	MERLIN	2001	DBLP DOI BibTeX RDF
1	Dale Miller 0001	Encoding Generic Judgments: Preliminary results.	MERLIN	2001	DBLP DOI BibTeX RDF
1	Simon Ambler, Roy L. Crole, Alberto Momigliano (eds.)	Mechanized Reasoning about Languages with Variable Binding, MERLIN 2001, in connection with IJCAR 2001, Siena, Italy, June 18, 2001	MERLIN	2001	DBLP BibTeX RDF

Publications at "MERLIN"( http://dblp.L3S.de/Venues/MERLIN )