|
|
Venues (Conferences, Journals, ...)
|
|
GrowBag graphs for keyword ? (Num. hits/coverage)
Group by:
The graphs summarize 51 occurrences of 34 keywords
|
|
|
Results
Found 29 publication records. Showing 29 according to the selection in the facets
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2005, Tallinn, Estonia, September 30, 2005, pp. 41-49, 2005, ACM, 978-1-59593-072-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2005, Tallinn, Estonia, September 30, 2005, pp. 13-24, 2005, ACM, 978-1-59593-072-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2005, Tallinn, Estonia, September 30, 2005, pp. 2-12, 2005, ACM, 978-1-59593-072-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2005, Tallinn, Estonia, September 30, 2005, pp. 25-32, 2005, ACM, 978-1-59593-072-9. The full citation details ...](Pics/full.jpeg) |
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 ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![ACM, 978-1-59593-072-9 The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Olha Shkaravska |
Types with semantics: soundness proof assistant. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2005, Tallinn, Estonia, September 30, 2005, pp. 50-57, 2005, ACM, 978-1-59593-072-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2005, Tallinn, Estonia, September 30, 2005, pp. 33-40, 2005, ACM, 978-1-59593-072-9. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
names, abstract syntax, scope, nominal logic |
1 | Frank Pfenning |
Towards a type theory of contexts. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2005, Tallinn, Estonia, September 30, 2005, pp. 1, 2005, ACM, 978-1-59593-072-9. The full citation details ...](Pics/full.jpeg) |
2005 |
DBLP DOI BibTeX RDF |
|
1 | Kevin Donnelly, Hongwei Xi |
Combining higher-order abstract syntax with first-order abstract syntax in ATS. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2005, Tallinn, Estonia, September 30, 2005, pp. 58-63, 2005, ACM, 978-1-59593-072-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2003, Uppsala, Sweden, August 2003, 2003, ACM, 978-1-58113-800-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2003, Uppsala, Sweden, August 2003, 2003, ACM, 978-1-58113-800-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2003, Uppsala, Sweden, August 2003, 2003, ACM, 978-1-58113-800-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2003, Uppsala, Sweden, August 2003, 2003, ACM, 978-1-58113-800-9. The full citation details ...](Pics/full.jpeg) |
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 ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![ACM, 978-1-58113-800-9 The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
|
1 | Alberto Momigliano, Jeff Polakow |
A formalization of an Ordered Logical Framework in Hybrid with applications to continuation machines. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2003, Uppsala, Sweden, August 2003, 2003, ACM, 978-1-58113-800-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2003, Uppsala, Sweden, August 2003, 2003, ACM, 978-1-58113-800-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2003, Uppsala, Sweden, August 2003, 2003, ACM, 978-1-58113-800-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2003, Uppsala, Sweden, August 2003, 2003, ACM, 978-1-58113-800-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2003, Uppsala, Sweden, August 2003, 2003, ACM, 978-1-58113-800-9. The full citation details ...](Pics/full.jpeg) |
2003 |
DBLP DOI BibTeX RDF |
linear logic, NP-complete problems, logical frameworks |
1 | Yasuhiko Minamide, Koji Okuma |
Verifying CPS transformations in Isabelle/HOL. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2003, Uppsala, Sweden, August 2003, 2003, ACM, 978-1-58113-800-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Eighth ACM SIGPLAN International Conference on Functional Programming, Workshop on Mechanized reasoning about languages with variable binding, MERLIN 2003, Uppsala, Sweden, August 2003, 2003, ACM, 978-1-58113-800-9. The full citation details ...](Pics/full.jpeg) |
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. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Mechanized Reasoning about Languages with Variable Binding, MERLIN 2001, in connection with IJCAR 2001, Siena, Italy, June 18, 2001, pp. 1-17, 2001, Elsevier. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Carsten Schürmann, Dachuan Yu, Zhaozhong Ni |
A Representation of Fomega in LF. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Mechanized Reasoning about Languages with Variable Binding, MERLIN 2001, in connection with IJCAR 2001, Siena, Italy, June 18, 2001, pp. 79-96, 2001, Elsevier. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Marino Miculan |
Developing (Meta)Theory of Lambda-calculus in the Theory of Context. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Mechanized Reasoning about Languages with Variable Binding, MERLIN 2001, in connection with IJCAR 2001, Siena, Italy, June 18, 2001, pp. 37-58, 2001, Elsevier. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Andreas Abel 0001 |
A Third-Order Representation of the lambda-mu-Calculus. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Mechanized Reasoning about Languages with Variable Binding, MERLIN 2001, in connection with IJCAR 2001, Siena, Italy, June 18, 2001, pp. 97-114, 2001, Elsevier. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
1 | René Vestergaard, James Brotherston |
The Mechanisation of Barendregt-Style Equational Proofs (the Residual Perspective). ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Mechanized Reasoning about Languages with Variable Binding, MERLIN 2001, in connection with IJCAR 2001, Siena, Italy, June 18, 2001, pp. 18-36, 2001, Elsevier. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Simon Ambler, Roy L. Crole, Alberto Momigliano |
Preface: Mechanised Reasoning about Languages with Variable Binding 2001. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Mechanized Reasoning about Languages with Variable Binding, MERLIN 2001, in connection with IJCAR 2001, Siena, Italy, June 18, 2001, pp. 115-116, 2001, Elsevier. The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP DOI BibTeX RDF |
|
1 | Dale Miller 0001 |
Encoding Generic Judgments: Preliminary results. ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![In: Mechanized Reasoning about Languages with Variable Binding, MERLIN 2001, in connection with IJCAR 2001, Siena, Italy, June 18, 2001, pp. 59-78, 2001, Elsevier. The full citation details ...](Pics/full.jpeg) |
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 ![Search on Bibsonomy](Pics/bibsonomy.png) |
MERLIN ![Elsevier The full citation details ...](Pics/full.jpeg) |
2001 |
DBLP BibTeX RDF |
|
Displaying result #1 - #29 of 29 (100 per page; Change: )
|
|