nad / chi Goto Github PK
View Code? Open in Web Editor NEWLicense: MIT License
License: MIT License
------------------------------------------------------------------------ -- A formalisation of one variant of the language χ, along with a -- number of properties -- -- Nils Anders Danielsson ------------------------------------------------------------------------ -- A description of the language χ, as well as some of the definitions -- and proofs used in this development, can be found in "The language -- χ" by Bengt Nordström (edited by me): -- -- * https://chalmers.instructure.com/courses/20908/file_contents/course%20files/reading/The_language_chi.pdf -- -- See also the following lecture slides: -- -- * https://chalmers.instructure.com/courses/20908/file_contents/course%20files/lectures/L4.pdf -- * https://chalmers.instructure.com/courses/20908/file_contents/course%20files/lectures/L5.pdf -- * https://chalmers.instructure.com/courses/20908/file_contents/course%20files/lectures/L6.pdf module README where -- Atoms. import Atom -- Various constants. import Constants -- A specification of the language χ. import Chi -- Some cancellation lemmas. import Cancellation -- The semantics is deterministic. import Deterministic -- Values. import Values -- "Reasoning" combinators. import Reasoning -- The abstract syntax is a set, and the semantics is propositional. import Propositional -- Compatibility lemmas. import Compatibility -- Some lemmas and definitions related to substitution. import Substitution -- Definitions of "free in" and "closed", along with some properties. import Free-variables -- Alpha-equivalence. import Alpha-equivalence -- Encoders and decoders. import Coding -- Encoder and decoder instances. import Coding.Instances -- Encoder and decoder instances for Atom.χ-ℕ-atoms. import Coding.Instances.Nat -- The "not the code of" operator ⌞_⌟. import Not-the-code-of -- A tactic that can "remove" applications of substitutions to closed -- expressions. import Free-variables.Remove-substs -- A definition of the size of an operational semantics derivation, -- along with some properties. import Derivation-size -- The "terminates" relation. import Termination -- Some χ program combinators. import Combinators -- A definition of the size of an expression, along with some -- properties. import Expression-size -- The rec construction can be encoded using λ-terms. import Recursion-without-rec -- Some aspects of the semantics are decidable. import Decidable -- Partial functions, computability. import Computability -- Computable Agda functions. import Computable-function -- Internal coding. import Internal-coding -- Internal substitution. import Internal-substitution -- Internal lookup. import Internal-lookup -- A self-interpreter. import Self-interpreter -- The halting problem. import Halting-problem -- Rice's theorem. import Rices-theorem -- Some results related to pointwise equality. import Pointwise-equality
I have version 85bbacd
of nad/equality
installed. Attempting to typecheck Chi.agda
fails with:
> agda Chi.agda
Checking Chi (/home/ayberkt/code/chi/src/Chi.agda).
Checking Atom (/home/ayberkt/code/chi/src/Atom.agda).
/home/ayberkt/code/chi/src/Atom.agda:16,40-55
(Equality.Equality-with-J _a_10 _p_11 equivalence-relation⁺) !=<
(Equality.Path.Equality-with-paths a p _e⁺_9)
when checking that the expression equality-with-J has type
Equality.Path.Equality-with-paths a p _e⁺_9
A declarative, efficient, and flexible JavaScript library for building user interfaces.
🖖 Vue.js is a progressive, incrementally-adoptable JavaScript framework for building UI on the web.
TypeScript is a superset of JavaScript that compiles to clean JavaScript output.
An Open Source Machine Learning Framework for Everyone
The Web framework for perfectionists with deadlines.
A PHP framework for web artisans
Bring data to life with SVG, Canvas and HTML. 📊📈🎉
JavaScript (JS) is a lightweight interpreted programming language with first-class functions.
Some thing interesting about web. New door for the world.
A server is a program made to process requests and deliver data to clients.
Machine learning is a way of modeling and interpreting data that allows a piece of software to respond intelligently.
Some thing interesting about visualization, use data art
Some thing interesting about game, make everyone happy.
We are working to build community through open source technology. NB: members must have two-factor auth.
Open source projects and samples from Microsoft.
Google ❤️ Open Source for everyone.
Alibaba Open Source for everyone
Data-Driven Documents codes.
China tencent open source team.