1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
|
@inproceedings{lafont1990interactionnets,
author = {Lafont, Yves},
title = {Interaction nets},
year = {1989},
isbn = {0897913434},
publisher = {Association for Computing Machinery},
address = {New York, NY, USA},
url = {https://doi.org/10.1145/96709.96718},
doi = {10.1145/96709.96718},
abstract = {We propose a new kind of programming language, with the following features:Interaction nets generalize Girard's proof nets of linear logic and illustrate the advantage of an integrated logic approach, as opposed to the external one. In other words, we did not try to design a logic describing the behaviour of some given computational system, but a programming language for which the type discipline is already (almost) a logic.In fact, we shall scarcely refer to logic, because we adopt a na\"{\i}ve and pragmatic style. A typical application we have in mind for this language is the design of interactive softwares such as editors or window managers.},
booktitle = {Proceedings of the 17th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages},
pages = {95–108},
numpages = {14},
location = {San Francisco, California, USA},
series = {POPL '90}
}
@inproceedings{demoura2008z3,
author="de Moura, Leonardo
and Bj{\o}rner, Nikolaj",
editor="Ramakrishnan, C. R.
and Rehof, Jakob",
title="Z3: An Efficient SMT Solver",
booktitle="Tools and Algorithms for the Construction and Analysis of Systems",
year="2008",
publisher="Springer Berlin Heidelberg",
address="Berlin, Heidelberg",
pages="337--340",
abstract="Satisfiability Modulo Theories (SMT) problem is a decision problem for logical first order formulas with respect to combinations of background theories such as: arithmetic, bit-vectors, arrays, and uninterpreted functions. Z3 is a new and efficient SMT Solver freely available from Microsoft Research. It is used in various software verification and analysis applications.",
isbn="978-3-540-78800-3"
}
|
