Name | Last modified | Size | Description | |
---|---|---|---|---|
Parent Directory | - | |||
Agda.Builtin.Bool.html | 2023-09-29 17:41 | 3.1K | ||
Agda.Primitive.html | 2023-09-29 17:41 | 5.4K | ||
Agda.css | 2023-09-29 17:41 | 1.8K | ||
Agda.Builtin.List.html | 2023-09-29 17:41 | 4.7K | ||
Agda.Builtin.Nat.html | 2023-09-29 17:41 | 23K | ||
Agda.Builtin.Unit.html | 2023-09-29 17:41 | 1.7K | ||
Agda.Builtin.Char.html | 2023-09-29 17:41 | 4.0K | ||
Agda.Builtin.Maybe.html | 2023-09-29 17:41 | 2.3K | ||
Agda.Builtin.Sigma.html | 2023-09-29 17:41 | 3.4K | ||
Agda.Builtin.String...> | 2023-09-29 17:41 | 10K | ||
Prelude.html | 2023-09-29 17:41 | 123K | ||
Logical-equivalence...> | 2023-09-29 17:41 | 50K | ||
Equality.html | 2023-09-29 17:41 | 1.0M | ||
Surjection.html | 2023-09-29 17:41 | 88K | ||
Nat.html | 2023-09-29 17:41 | 476K | ||
H-level.html | 2023-09-29 17:41 | 53K | ||
Equality.Decidable-U..> | 2023-09-29 17:41 | 76K | ||
Equality.Decision-pr..> | 2023-09-29 17:41 | 97K | ||
Injection.html | 2023-09-29 17:41 | 18K | ||
Bijection.html | 2023-09-29 17:41 | 226K | ||
Preimage.html | 2023-09-29 17:41 | 59K | ||
Equivalence.Contract..> | 2023-09-29 17:41 | 128K | ||
Equivalence.Half-adj..> | 2023-09-29 17:41 | 133K | ||
Extensionality.html | 2023-09-29 17:41 | 189K | ||
Erased.Basics.html | 2023-09-29 17:41 | 14K | ||
H-level.Closure.html | 2023-09-29 17:41 | 406K | ||
Agda.Builtin.Int.html | 2023-09-29 17:41 | 3.4K | ||
Equivalence.Erased.C..> | 2023-09-29 17:41 | 70K | ||
Integer.Basics.html | 2023-09-29 17:41 | 40K | ||
Groupoid.html | 2023-09-29 17:41 | 189K | ||
Equivalence.html | 2023-09-29 17:41 | 502K | ||
Equivalence.Erased.B..> | 2023-09-29 17:41 | 97K | ||
Excluded-middle.html | 2023-09-29 17:41 | 6.6K | ||
Embedding.html | 2023-09-29 17:41 | 82K | ||
Function-universe.html | 2023-09-29 17:41 | 2.5M | ||
Monad.Raw.html | 2023-09-29 17:41 | 18K | ||
Agda.Builtin.Equalit..> | 2023-09-29 17:41 | 2.6K | ||
Monad.html | 2023-09-29 17:41 | 115K | ||
Agda.Builtin.Size.html | 2023-09-29 17:41 | 4.2K | ||
Equality.Proposition..> | 2023-09-29 17:41 | 19K | ||
Prelude.Size.html | 2023-09-29 17:41 | 3.1K | ||
Conat.html | 2023-09-29 17:41 | 432K | ||
Delay-monad.html | 2023-09-29 17:41 | 16K | ||
Delay-monad.Bisimila..> | 2023-09-29 17:41 | 9.0K | ||
Maybe.html | 2023-09-29 17:41 | 52K | ||
Delay-monad.Bisimila..> | 2023-09-29 17:41 | 246K | ||
Delay-monad.Monad.html | 2023-09-29 17:41 | 61K | ||
Delay-monad.Sequenti..> | 2023-09-29 17:41 | 104K | ||
Delay-monad.Parallel..> | 2023-09-29 17:41 | 137K | ||
Accessibility.html | 2023-09-29 17:41 | 94K | ||
Bool.html | 2023-09-29 17:41 | 74K | ||
Erased.Box-cong-axio..> | 2023-09-29 17:41 | 7.0K | ||
Univalence-axiom.html | 2023-09-29 17:41 | 706K | ||
Equivalence-relation..> | 2023-09-29 17:41 | 82K | ||
Level.html | 2023-09-29 17:41 | 5.6K | ||
Data.Empty.html | 2023-09-29 17:41 | 4.1K | ||
Data.Irrelevant.html | 2023-09-29 17:41 | 12K | ||
Data.Unit.Base.html | 2023-09-29 17:41 | 1.9K | ||
Function.Base.html | 2023-09-29 17:41 | 75K | ||
Data.Bool.Base.html | 2023-09-29 17:41 | 13K | ||
Data.Empty.Irrelevan..> | 2023-09-29 17:41 | 2.2K | ||
Data.Sum.Base.html | 2023-09-29 17:41 | 26K | ||
Data.Product.Base.html | 2023-09-29 17:41 | 87K | ||
Relation.Nullary.Neg..> | 2023-09-29 17:41 | 21K | ||
Data.These.Base.html | 2023-09-29 17:41 | 36K | ||
Relation.Nullary.Ref..> | 2023-09-29 17:41 | 34K | ||
Relation.Nullary.Dec..> | 2023-09-29 17:41 | 56K | ||
Data.Maybe.Base.html | 2023-09-29 17:41 | 37K | ||
Relation.Binary.Core..> | 2023-09-29 17:41 | 19K | ||
Relation.Binary.Defi..> | 2023-09-29 17:41 | 91K | ||
Relation.Binary.Prop..> | 2023-09-29 17:41 | 45K | ||
Relation.Binary.Inde..> | 2023-09-29 17:41 | 13K | ||
Relation.Binary.Inde..> | 2023-09-29 17:41 | 10K | ||
Relation.Binary.Inde..> | 2023-09-29 17:41 | 13K | ||
Relation.Binary.Inde..> | 2023-09-29 17:41 | 11K | ||
Relation.Binary.Inde..> | 2023-09-29 17:41 | 2.1K | ||
Relation.Nullary.html | 2023-09-29 17:41 | 6.5K | ||
Relation.Unary.html | 2023-09-29 17:41 | 91K | ||
Relation.Binary.Cons..> | 2023-09-29 17:41 | 101K | ||
Effect.Empty.html | 2023-09-29 17:41 | 3.4K | ||
Relation.Binary.Stru..> | 2023-09-29 17:41 | 62K | ||
Data.Unit.Polymorphi..> | 2023-09-29 17:41 | 3.3K | ||
Effect.Choice.html | 2023-09-29 17:41 | 4.4K | ||
Effect.Functor.html | 2023-09-29 17:41 | 13K | ||
Effect.Applicative.html | 2023-09-29 17:41 | 36K | ||
Effect.Monad.html | 2023-09-29 17:41 | 32K | ||
Relation.Nullary.Neg..> | 2023-09-29 17:41 | 38K | ||
Relation.Binary.Bund..> | 2023-09-29 17:41 | 66K | ||
Algebra.Core.html | 2023-09-29 17:41 | 3.3K | ||
Relation.Binary.html | 2023-09-29 17:41 | 1.9K | ||
Algebra.Definitions...> | 2023-09-29 17:41 | 118K | ||
Relation.Binary.Reas..> | 2023-09-29 17:41 | 20K | ||
Relation.Binary.Reas..> | 2023-09-29 17:41 | 7.4K | ||
Algebra.Consequences..> | 2023-09-29 17:41 | 7.1K | ||
Function.Definitions..> | 2023-09-29 17:41 | 21K | ||
Algebra.Consequences..> | 2023-09-29 17:41 | 165K | ||
Algebra.Structures.html | 2023-09-29 17:41 | 210K | ||
Algebra.Structures.B..> | 2023-09-29 17:41 | 64K | ||
Algebra.Bundles.Raw...> | 2023-09-29 17:41 | 54K | ||
Algebra.Bundles.html | 2023-09-29 17:41 | 255K | ||
Algebra.html | 2023-09-29 17:41 | 1.9K | ||
Relation.Binary.Prop..> | 2023-09-29 17:41 | 18K | ||
Relation.Binary.Inde..> | 2023-09-29 17:41 | 15K | ||
Relation.Binary.Prop..> | 2023-09-29 17:41 | 5.5K | ||
Relation.Binary.Prop..> | 2023-09-29 17:41 | 104K | ||
Function.Equality.html | 2023-09-29 17:41 | 40K | ||
Function.Consequence..> | 2023-09-29 17:41 | 22K | ||
Function.Consequence..> | 2023-09-29 17:41 | 34K | ||
Function.Structures...> | 2023-09-29 17:41 | 43K | ||
Function.Bundles.html | 2023-09-29 17:41 | 110K | ||
Axiom.UniquenessOfId..> | 2023-09-29 17:41 | 23K | ||
Relation.Nullary.Dec..> | 2023-09-29 17:41 | 32K | ||
Axiom.Extensionality..> | 2023-09-29 17:41 | 21K | ||
Data.Parity.Base.html | 2023-09-29 17:41 | 19K | ||
Data.Sign.Base.html | 2023-09-29 17:41 | 8.9K | ||
Relation.Binary.Prop..> | 2023-09-29 17:41 | 53K | ||
Data.Nat.Base.html | 2023-09-29 17:41 | 83K | ||
Data.Fin.Base.html | 2023-09-29 17:41 | 117K | ||
Data.List.Base.html | 2023-09-29 17:41 | 194K | ||
Data.Vec.Base.html | 2023-09-29 17:41 | 153K | ||
Data.Vec.N-ary.html | 2023-09-29 17:41 | 92K | ||
Relation.Binary.Refl..> | 2023-09-29 17:41 | 37K | ||
Algebra.Properties.A..> | 2023-09-29 17:41 | 12K | ||
Algebra.Properties.G..> | 2023-09-29 17:41 | 52K | ||
Function.Core.html | 2023-09-29 17:41 | 5.0K | ||
Relation.Binary.Morp..> | 2023-09-29 17:41 | 6.3K | ||
Relation.Binary.Morp..> | 2023-09-29 17:41 | 38K | ||
Algebra.Morphism.Def..> | 2023-09-29 17:41 | 11K | ||
Algebra.Morphism.Str..> | 2023-09-29 17:41 | 177K | ||
Algebra.Morphism.html | 2023-09-29 17:41 | 47K | ||
Algebra.Properties.R..> | 2023-09-29 17:41 | 41K | ||
Algebra.Solver.Ring...> | 2023-09-29 17:41 | 43K | ||
Relation.Binary.Cons..> | 2023-09-29 17:41 | 72K | ||
Relation.Binary.Prop..> | 2023-09-29 17:41 | 9.8K | ||
Relation.Binary.Cons..> | 2023-09-29 17:41 | 69K | ||
Relation.Binary.Prop..> | 2023-09-29 17:41 | 34K | ||
Algebra.Construct.Na..> | 2023-09-29 17:41 | 17K | ||
Relation.Binary.Prop..> | 2023-09-29 17:41 | 17K | ||
Algebra.Consequences..> | 2023-09-29 17:41 | 39K | ||
Algebra.Lattice.Stru..> | 2023-09-29 17:41 | 41K | ||
Relation.Binary.Reas..> | 2023-09-29 17:41 | 45K | ||
Relation.Binary.Reas..> | 2023-09-29 17:41 | 3.5K | ||
Algebra.Construct.Na..> | 2023-09-29 17:41 | 109K | ||
Algebra.Lattice.Bund..> | 2023-09-29 17:41 | 7.2K | ||
Algebra.Construct.Na..> | 2023-09-29 17:41 | 18K | ||
Algebra.Lattice.Bund..> | 2023-09-29 17:41 | 51K | ||
Algebra.Lattice.Cons..> | 2023-09-29 17:41 | 6.3K | ||
Algebra.Construct.Na..> | 2023-09-29 17:41 | 57K | ||
Algebra.Lattice.Cons..> | 2023-09-29 17:41 | 4.5K | ||
Algebra.Lattice.Cons..> | 2023-09-29 17:41 | 18K | ||
Data.Unit.Properties..> | 2023-09-29 17:41 | 16K | ||
Data.Unit.html | 2023-09-29 17:41 | 1.7K | ||
Algebra.Properties.S..> | 2023-09-29 17:41 | 8.2K | ||
Relation.Binary.Reas..> | 2023-09-29 17:41 | 69K | ||
Algebra.Properties.C..> | 2023-09-29 17:41 | 112K | ||
Function.Metric.Core..> | 2023-09-29 17:41 | 2.8K | ||
Function.Metric.Defi..> | 2023-09-29 17:41 | 35K | ||
Function.Metric.Stru..> | 2023-09-29 17:41 | 22K | ||
Function.Metric.Bund..> | 2023-09-29 17:41 | 37K | ||
Function.Metric.Nat...> | 2023-09-29 17:41 | 2.6K | ||
Function.Metric.Nat...> | 2023-09-29 17:41 | 17K | ||
Function.Metric.Nat...> | 2023-09-29 17:41 | 28K | ||
Function.Metric.Nat...> | 2023-09-29 17:41 | 18K | ||
Function.Metric.Nat...> | 2023-09-29 17:41 | 1.8K | ||
Function.Equivalence..> | 2023-09-29 17:41 | 40K | ||
Induction.html | 2023-09-29 17:41 | 17K | ||
Induction.WellFounde..> | 2023-09-29 17:41 | 87K | ||
Relation.Binary.Latt..> | 2023-09-29 17:41 | 12K | ||
Relation.Binary.Latt..> | 2023-09-29 17:41 | 61K | ||
Relation.Binary.Latt..> | 2023-09-29 17:41 | 68K | ||
Relation.Binary.Latt..> | 2023-09-29 17:41 | 1.7K | ||
Relation.Binary.Cons..> | 2023-09-29 17:41 | 77K | ||
Algebra.Lattice.Prop..> | 2023-09-29 17:41 | 11K | ||
Algebra.Lattice.Prop..> | 2023-09-29 17:41 | 6.0K | ||
Algebra.Lattice.Prop..> | 2023-09-29 17:41 | 42K | ||
Algebra.Lattice.Prop..> | 2023-09-29 17:41 | 293K | ||
Data.Bool.Properties..> | 2023-09-29 17:41 | 204K | ||
Data.Nat.Properties...> | 2023-09-29 17:41 | 908K | ||
Algebra.Definitions...> | 2023-09-29 17:41 | 16K | ||
Algebra.Definitions...> | 2023-09-29 17:41 | 11K | ||
Data.Vec.Functional...> | 2023-09-29 17:41 | 69K | ||
Algebra.Definitions...> | 2023-09-29 17:41 | 21K | ||
Algebra.Properties.M..> | 2023-09-29 17:41 | 30K | ||
Data.Nat.html | 2023-09-29 17:41 | 5.7K | ||
Algebra.Properties.S..> | 2023-09-29 17:41 | 38K | ||
Algebra.Solver.Ring...> | 2023-09-29 17:41 | 96K | ||
Algebra.Solver.Ring...> | 2023-09-29 17:41 | 4.3K | ||
Algebra.Solver.Ring...> | 2023-09-29 17:41 | 294K | ||
Data.Nat.Solver.html | 2023-09-29 17:41 | 2.4K | ||
Data.List.Membership..> | 2023-09-29 17:41 | 19K | ||
Data.List.Relation.U..> | 2023-09-29 17:41 | 38K | ||
Data.List.Relation.B..> | 2023-09-29 17:41 | 2.8K | ||
Data.List.Relation.B..> | 2023-09-29 17:41 | 10K | ||
Relation.Binary.Cons..> | 2023-09-29 17:41 | 83K | ||
Algebra.Construct.Li..> | 2023-09-29 17:41 | 83K | ||
Algebra.Construct.Na..> | 2023-09-29 17:41 | 13K | ||
Algebra.Construct.Na..> | 2023-09-29 17:41 | 7.3K | ||
Data.List.Extrema.Co..> | 2023-09-29 17:41 | 60K | ||
Data.Sum.Properties...> | 2023-09-29 17:41 | 60K | ||
Data.Product.Propert..> | 2023-09-29 17:41 | 55K | ||
Data.Unit.Polymorphi..> | 2023-09-29 17:41 | 23K | ||
Data.Unit.Polymorphi..> | 2023-09-29 17:41 | 1.9K | ||
Function.Construct.I..> | 2023-09-29 17:41 | 45K | ||
Function.Construct.C..> | 2023-09-29 17:41 | 115K | ||
Function.Construct.S..> | 2023-09-29 17:41 | 72K | ||
Data.Empty.Polymorph..> | 2023-09-29 17:41 | 3.8K | ||
Data.Sum.Algebra.html | 2023-09-29 17:41 | 30K | ||
Function.Properties...> | 2023-09-29 17:41 | 28K | ||
Data.Fin.Patterns.html | 2023-09-29 17:41 | 4.3K | ||
Data.Product.Algebra..> | 2023-09-29 17:41 | 52K | ||
Relation.Unary.Prope..> | 2023-09-29 17:41 | 113K | ||
Data.Fin.Properties...> | 2023-09-29 17:41 | 540K | ||
Data.Nat.DivMod.Core..> | 2023-09-29 17:41 | 222K | ||
Data.Nat.Induction.html | 2023-09-29 17:41 | 25K | ||
Data.Nat.Divisibilit..> | 2023-09-29 17:41 | 15K | ||
Data.Nat.DivMod.html | 2023-09-29 17:41 | 363K | ||
Data.Nat.Divisibilit..> | 2023-09-29 17:41 | 158K | ||
Data.List.Membership..> | 2023-09-29 17:41 | 9.3K | ||
Data.Product.Relatio..> | 2023-09-29 17:41 | 5.4K | ||
Data.List.Relation.U..> | 2023-09-29 17:41 | 110K | ||
Data.List.Properties..> | 2023-09-29 17:41 | 618K | ||
Function.Injection.html | 2023-09-29 17:41 | 23K | ||
Function.LeftInverse..> | 2023-09-29 17:41 | 42K | ||
Function.Surjection...> | 2023-09-29 17:41 | 33K | ||
Function.Bijection.html | 2023-09-29 17:41 | 33K | ||
Function.Inverse.html | 2023-09-29 17:41 | 60K | ||
Function.Properties...> | 2023-09-29 17:41 | 7.7K | ||
Function.Properties...> | 2023-09-29 17:41 | 20K | ||
Function.Properties...> | 2023-09-29 17:41 | 13K | ||
Function.Related.Pro..> | 2023-09-29 17:41 | 126K | ||
Function.Related.html | 2023-09-29 17:41 | 163K | ||
Data.Product.Relatio..> | 2023-09-29 17:41 | 113K | ||
Data.Product.Functio..> | 2023-09-29 17:41 | 55K | ||
Function.HalfAdjoint..> | 2023-09-29 17:41 | 46K | ||
Relation.Nullary.Ind..> | 2023-09-29 17:41 | 3.2K | ||
Data.Product.Functio..> | 2023-09-29 17:41 | 36K | ||
Data.Sum.Relation.Bi..> | 2023-09-29 17:41 | 111K | ||
Data.Sum.Function.Se..> | 2023-09-29 17:41 | 56K | ||
Data.Sum.Function.Pr..> | 2023-09-29 17:41 | 34K | ||
Function.Related.Typ..> | 2023-09-29 17:41 | 185K | ||
Data.List.Relation.U..> | 2023-09-29 17:41 | 6.3K | ||
Data.Product.Functio..> | 2023-09-29 17:41 | 159K | ||
Relation.Binary.Cons..> | 2023-09-29 17:41 | 78K | ||
Data.List.Relation.U..> | 2023-09-29 17:41 | 36K | ||
Data.List.Relation.U..> | 2023-09-29 17:41 | 5.7K | ||
Data.List.Relation.B..> | 2023-09-29 17:41 | 26K | ||
Data.List.Relation.B..> | 2023-09-29 17:41 | 37K | ||
Data.List.Relation.B..> | 2023-09-29 17:41 | 127K | ||
Data.List.Relation.B..> | 2023-09-29 17:41 | 48K | ||
Data.List.Effectful...> | 2023-09-29 17:41 | 142K | ||
Data.Maybe.Relation...> | 2023-09-29 17:41 | 31K | ||
Data.List.Membership..> | 2023-09-29 17:41 | 36K | ||
Data.List.Relation.U..> | 2023-09-29 17:41 | 452K | ||
Data.List.Membership..> | 2023-09-29 17:41 | 227K | ||
Data.List.Relation.B..> | 2023-09-29 17:41 | 6.3K | ||
Relation.Binary.Prop..> | 2023-09-29 17:41 | 15K | ||
Data.List.Membership..> | 2023-09-29 17:41 | 202K | ||
Data.List.Extrema.html | 2023-09-29 17:41 | 132K | ||
Data.Maybe.Relation...> | 2023-09-29 17:41 | 54K | ||
Data.List.Relation.U..> | 2023-09-29 17:41 | 411K | ||
Data.Vec.Bounded.Bas..> | 2023-09-29 17:41 | 68K | ||
Data.Vec.html | 2023-09-29 17:41 | 12K | ||
Equality.Instances-r..> | 2023-09-29 17:41 | 120K | ||
Nat.Solver.html | 2023-09-29 17:41 | 59K | ||
List.html | 2023-09-29 17:41 | 265K | ||
For-iterated-equalit..> | 2023-09-29 17:41 | 337K | ||
Equivalence.List.html | 2023-09-29 17:41 | 355K | ||
Pullback.html | 2023-09-29 17:41 | 102K | ||
Equivalence.Path-spl..> | 2023-09-29 17:41 | 413K | ||
Vec.Dependent.html | 2023-09-29 17:41 | 47K | ||
Modality.Basics.html | 2023-09-29 17:41 | 2.1M | ||
Erased.Level-1.html | 2023-09-29 17:41 | 1.0M | ||
Double-negation.html | 2023-09-29 17:41 | 96K | ||
Delay-monad.Terminat..> | 2023-09-29 17:41 | 42K | ||
Lambda.Delay-crash.html | 2023-09-29 17:41 | 144K | ||
Vec.Data.html | 2023-09-29 17:41 | 39K | ||
Agda.Builtin.Word.html | 2023-09-29 17:41 | 2.0K | ||
Lambda.Interpreter.html | 2023-09-29 17:41 | 24K | ||
Lambda.Syntax.html | 2023-09-29 17:41 | 43K | ||
Lambda.Virtual-machi..> | 2023-09-29 17:41 | 12K | ||
Agda.Builtin.Float.html | 2023-09-29 17:41 | 32K | ||
Agda.Builtin.Reflect..> | 2023-09-29 17:41 | 160K | ||
Agda.Builtin.Strict...> | 2023-09-29 17:41 | 4.8K | ||
TC-monad.html | 2023-09-29 17:41 | 170K | ||
Monad.State.html | 2023-09-29 17:41 | 37K | ||
Tactic.By.html | 2023-09-29 17:41 | 145K | ||
Tactic.By.Propositio..> | 2023-09-29 17:41 | 121K | ||
Lambda.Compiler.html | 2023-09-29 17:41 | 33K | ||
Colist.html | 2023-09-29 17:41 | 375K | ||
Lambda.Delay-crash-t..> | 2023-09-29 17:41 | 100K | ||
Lambda.Virtual-machi..> | 2023-09-29 17:41 | 36K | ||
Lambda.Compiler-corr..> | 2023-09-29 17:41 | 173K | ||
Omniscience.html | 2023-09-29 17:41 | 55K | ||
Upper-bounds.html | 2023-09-29 17:41 | 299K | ||
Lambda.Interpreter.S..> | 2023-09-29 17:41 | 130K | ||
Lambda.Interpreter.S..> | 2023-09-29 17:41 | 41K | ||
Only-allocation.html | 2023-09-29 17:41 | 6.9K | ||
Bounded-space.html | 2023-09-29 17:41 | 91K | ||
Unbounded-space.html | 2023-09-29 17:41 | 191K | ||
Lambda.Compiler-corr..> | 2023-09-29 17:41 | 257K | ||
Lambda.Interpreter.S..> | 2023-09-29 17:41 | 15K | ||
Delay-monad.Quantita..> | 2023-09-29 17:41 | 426K | ||
Lambda.Interpreter.S..> | 2023-09-29 17:41 | 35K | ||
Lambda.Compiler-corr..> | 2023-09-29 17:41 | 241K | ||
Lambda.Interpreter.S..> | 2023-09-29 17:41 | 34K | ||
Delay-monad.Always.html | 2023-09-29 17:41 | 14K | ||
Lambda.Type-soundnes..> | 2023-09-29 17:41 | 52K | ||
------------------------------------------------------------------------ -- Code related to the paper "Total Definitional Interpreters for Time -- and Space Complexity" -- -- Nils Anders Danielsson ------------------------------------------------------------------------ -- Note that the code has evolved after the paper was written. For -- code that is closer to the paper, see the version of the code that -- is distributed with the paper. module README where ------------------------------------------------------------------------ -- Pointers to results from the paper -- In order to more easily find code corresponding to results from the -- paper, see the following module. Note that some of the code -- referenced below is not discussed at all in the paper. import README.Pointers-to-results-from-the-paper ------------------------------------------------------------------------ -- Responses to some challenges from Ancona, Dagnino and Zucca -- The syntax of a toy programming language that only supports -- allocation and deallocation of memory. import Only-allocation -- Definitional interpreters can model systems with bounded space. import Bounded-space -- Upper bounds of colists containing natural numbers. import Upper-bounds -- Definitional interpreters can model systems with unbounded space. import Unbounded-space ------------------------------------------------------------------------ -- An example involving a simple λ-calculus -- Some developments based on "Operational Semantics Using the -- Partiality Monad" by Danielsson. -- -- These developments to a large extent mirror developments in -- "Coinductive big-step operational semantics" by Leroy and Grall. -- -- The main differences compared to those two pieces of work are -- perhaps the following ones: -- -- * Sized types are used. -- -- * The infinite set of uninterpreted constants has been replaced by -- booleans, and definitions (named, unary, recursive functions) -- are included. -- -- * The virtual machine and the compiler include support for tail -- calls. -- -- * Stack space usage is analysed. -- The syntax of, and a type system for, an untyped λ-calculus with -- booleans and recursive unary function calls. import Lambda.Syntax -- A delay monad with the possibility of crashing. import Lambda.Delay-crash -- A definitional interpreter. import Lambda.Interpreter -- A type soundness result. import Lambda.Type-soundness -- A combination of the delay monad (with the possibility of crashing) -- and a kind of writer monad yielding colists. import Lambda.Delay-crash-trace -- Virtual machine instructions, state etc. import Lambda.Virtual-machine.Instructions -- A virtual machine. import Lambda.Virtual-machine -- A compiler. import Lambda.Compiler -- Compiler correctness. import Lambda.Compiler-correctness -- A definitional interpreter that is instrumented with information -- about the stack size of the compiled program. import Lambda.Interpreter.Stack-sizes -- The actual maximum stack size of the compiled program matches the -- maximum stack size of the instrumented source-level semantics. import Lambda.Compiler-correctness.Sizes-match -- An example: A non-terminating program that runs in bounded stack -- space. import Lambda.Interpreter.Stack-sizes.Example -- A counterexample: The trace of stack sizes produced by the virtual -- machine is not necessarily bisimilar to that produced by the -- instrumented interpreter. import Lambda.Interpreter.Stack-sizes.Counterexample -- A counterexample: The number of steps taken by the uninstrumented -- interpreter is not, in general, linear in the number of steps taken -- by the virtual machine for the corresponding compiled program. import Lambda.Interpreter.Steps.Counterexample -- A definitional interpreter that is instrumented with information -- about the number of steps required to run the compiled program. import Lambda.Interpreter.Steps -- The "time complexity" of the compiled program matches the one -- obtained from the instrumented interpreter. import Lambda.Compiler-correctness.Steps-match